An interchange law for squares and cleanups to Cubical/PathSquare.v #3886
Annotations
3 errors and 10 warnings
|
|
|
Build HoTT
The operation was canceled.
|
|
|
|
Build HoTT:
theories/Basics/Overture.v#L199
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L190
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L189
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L142
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L76
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
Build HoTT:
theories/Basics/Overture.v#L74
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L73
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
Build HoTT:
theories/Basics/Settings.v#L52
There is no flag or option with this name: "Loose Hint Behavior".
|
|
Build HoTT:
theories/Basics/Settings.v#L10
"coq-core" has been renamed to "rocq-runtime".
|
|
Build HoTT:
theories/Basics/Settings.v#L8
"coq-core" has been renamed to "rocq-runtime".
|
Loading