diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_11890.v | 10 |
1 files changed, 10 insertions, 0 deletions
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. +*) |