diff options
| author | Hugo Herbelin | 2020-03-26 08:45:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-26 08:45:43 +0100 |
| commit | 84f6394f78baea5b1f261765164ae23cd245a357 (patch) | |
| tree | d7a0b4da8708f5f261f66c8ccd6ed1c48cafd988 /test-suite | |
| parent | 1217583de0c7ac0d17c8917f21c30c247176d83f (diff) | |
| parent | 528dd28a48dd7b1898212e2aae9b43bb19fb91cc (diff) | |
Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlib
Reviewed-by: herbelin
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. +*) |