From 0629f875fb9d7610075d657a259a4aa1d2b24b33 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 19 Mar 2024 14:20:41 +0100 Subject: [PATCH] Ad-hoc fix to recover the compatibility with coq-dev (8.20) --- theories/ordered_qelim.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/theories/ordered_qelim.v b/theories/ordered_qelim.v index 11b9f8a..0a8aa54 100644 --- a/theories/ordered_qelim.v +++ b/theories/ordered_qelim.v @@ -172,15 +172,13 @@ 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. +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