Adapt to Rocq#21180 #2315
+40
−38
Open
Adapt to Rocq#21180 #2315
Annotations
10 warnings
|
theories/Basics/Overture.v#L199
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
theories/Basics/Overture.v#L190
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
theories/Basics/Overture.v#L189
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
theories/Basics/Overture.v#L142
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
theories/Basics/Overture.v#L76
Implicitly declaring hint databases is deprecated. Please explicitly
|
|
theories/Basics/Overture.v#L74
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
theories/Basics/Overture.v#L73
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
theories/Basics/Settings.v#L54
There is no flag or option with this name: "Loose Hint Behavior".
|
|
theories/Basics/Settings.v#L12
"coq-core" has been renamed to "rocq-runtime".
|
|
theories/Basics/Settings.v#L10
"coq-core" has been renamed to "rocq-runtime".
|
The logs for this run have expired and are no longer available.
Loading