Merge PR #11635: Cleanup around the tolerability structure

Reviewed-by: ejgallego

1 files changed, 7 insertions, 7 deletions

diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index a84d2a4cb0..b6699493bb 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -12,7 +12,7 @@ open Pp
 open CErrors
 open Util
 open Notation
-open Notation_gram
+open Constrexpr
 
 (* Register the level of notation for parsing and printing
    (also register the parsing rule if not onlyprinting) *)
@@ -37,10 +37,11 @@ let get_defined_notations () =
 
 open Extend
 
-let parenRelation_eq t1 t2 = match t1, t2 with
-| L, L | E, E | Any, Any -> true
-| Prec l1, Prec l2 -> Int.equal l1 l2
-| _ -> false
+let entry_relative_level_eq t1 t2 = match t1, t2 with
+| LevelLt n1, LevelLt n2 -> Int.equal n1 n2
+| LevelLe n1, LevelLe n2 -> Int.equal n1 n2
+| LevelSome, LevelSome -> true
+| (LevelLt _ | LevelLe _ | LevelSome), _ -> false
 
 let production_position_eq pp1 pp2 = match (pp1,pp2) with
 | BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
@@ -64,11 +65,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
 let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
-  let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
   let prod_eq (l1,pp1) (l2,pp2) =
     not strict ||
     (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
-  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
   && List.equal (constr_entry_key_eq prod_eq) u1 u2
 
 let level_eq = level_eq_gen false