diff options
| -rw-r--r-- | doc/changelog/10-standard-library/11891-fix-order-notations.rst | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_11890.v | 10 | ||||
| -rw-r--r-- | theories/Sorting/Mergesort.v | 3 | ||||
| -rw-r--r-- | theories/Structures/Orders.v | 4 |
4 files changed, 23 insertions, 4 deletions
diff --git a/doc/changelog/10-standard-library/11891-fix-order-notations.rst b/doc/changelog/10-standard-library/11891-fix-order-notations.rst new file mode 100644 index 0000000000..d58d26244a --- /dev/null +++ b/doc/changelog/10-standard-library/11891-fix-order-notations.rst @@ -0,0 +1,10 @@ +- **Changed:** + Notations :g:`<=?` and :g:`<?` from ``Coq.Structures.Orders`` and + ``Coq.Sorting.Mergesort.NatOrder`` are now at level 70 rather than + 35, so as to be compatible with the notations defined everywhere + else in the standard library. This may require re-parenthesizing + some expressions. These notations were breaking the ability to + import modules from the standard library that were otherwise + compatible (fixes `#11890 + <https://github.com/coq/coq/issues/11890>`_, `#11891 + <https://github.com/coq/coq/pull/11891>`_, by Jason Gross). diff --git a/test-suite/bugs/closed/bug_11890.v b/test-suite/bugs/closed/bug_11890.v new file mode 100644 index 0000000000..c0426fcfda --- /dev/null +++ b/test-suite/bugs/closed/bug_11890.v @@ -0,0 +1,10 @@ +Require Import Coq.Structures.Orders Coq.ZArith.ZArith Coq.Sorting.Mergesort. +(* Note that this has always worked fine without the '; we are testing importing notations from the stdlib here *) +Declare Module A : LeBool'. +Declare Module B : LtBool'. +Import A B NatOrder. +(* +Error: Notation "_ <=? _" is already defined at level 70 with arguments constr +at next level, constr at next level while it is now required to be at level 35 +with arguments constr at next level, constr at next level. +*) diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v index a761dba62d..e9171cfdb3 100644 --- a/theories/Sorting/Mergesort.v +++ b/theories/Sorting/Mergesort.v @@ -259,7 +259,7 @@ Module NatOrder <: TotalLeBool. | _, 0 => false | S x', S y' => leb x' y' end. - Infix "<=?" := leb (at level 35). + Infix "<=?" := leb (at level 70, no associativity). Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1. Proof. induction a1; destruct a2; simpl; auto. @@ -269,4 +269,3 @@ End NatOrder. Module Import NatSort := Sort NatOrder. Example SimpleMergeExample := Eval compute in sort [5;3;6;1;8;6;0]. - diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 6a0e7397eb..94938c1d4d 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -192,11 +192,11 @@ Module Type HasLtb (Import T:Typ). End HasLtb. Module Type LebNotation (T:Typ)(E:HasLeb T). - Infix "<=?" := E.leb (at level 35). + Infix "<=?" := E.leb (at level 70, no associativity). End LebNotation. Module Type LtbNotation (T:Typ)(E:HasLtb T). - Infix "<?" := E.ltb (at level 35). + Infix "<?" := E.ltb (at level 70, no associativity). End LtbNotation. Module Type LebSpec (T:Typ)(X:HasLe T)(Y:HasLeb T). |