Ad-hoc fix to recover the compatibility with coq-dev (8.20)

math-comp · Mar 19, 2024 · 2f72f42 · 2f72f42
1 parent a1691eb
commit 2f72f42
Showing 1 changed file with 5 additions and 6 deletions.
diff --git a/theories/ordered_qelim.v b/theories/ordered_qelim.v
@@ -172,15 +172,14 @@ Declare Scope oclause_scope.
 Delimit Scope oclause_scope with OCLAUSE.
 Open Scope oclause_scope.
 
-Notation "p .1" := (@eq_of_oclause _ p)
-  (at level 2, left associativity, format "p .1") : oclause_scope.
-Notation "p .2" := (@neq_of_oclause _ p)
-  (at level 2, left associativity, format "p .2") : oclause_scope.
+(* TODO: add `at level 1, left associativity` when dropping the support for Coq 8.19 *)
+Notation "p .1" := (@eq_of_oclause _ p) (format "p .1") : oclause_scope.
+Notation "p .2" := (@neq_of_oclause _ p) (format "p .2") : oclause_scope.
 
 Notation "p .3" := (@lt_of_oclause _ p)
-  (at level 2, left associativity, format "p .3") : oclause_scope.
+  (at level 1, left associativity, format "p .3") : oclause_scope.
 Notation "p .4" := (@le_of_oclause _ p)
-  (at level 2, left associativity, format "p .4") : oclause_scope.
+  (at level 1, left associativity, format "p .4") : oclause_scope.
 
 Definition oclause_eq (T : eqType)(t1 t2 : oclause T) :=
   let: Oclause eq_l1 neq_l1 lt_l1 leq_l1 := t1 in