Theorem 5.8.2 from the book: characterizations of identity types #3035
Annotations
2 warnings
|
Run coq-community/docker-coq-action@v1:
theories/Basics/Settings.v#L10
Legacy loading plugin method has been removed from Coq, and the `:` syntax is deprecated, and its first argument ignored; please remove "ltac_plugin:" from your Declare ML
|
|
Run coq-community/docker-coq-action@v1:
theories/Basics/Settings.v#L12
Legacy loading plugin method has been removed from Coq, and the `:` syntax is deprecated, and its first argument ignored; please remove "number_string_notation_plugin:" from your Declare ML
|
Loading