diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 13ff960f64..ea7ef21b19 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -97,9 +97,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETBigint, ETBigint -> true | ETBinder b1, ETBinder b2 -> b1 == b2 | ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 -| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2 +| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 +| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 | ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' -| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false +| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in @@ -626,10 +627,10 @@ let availability_of_prim_token n printer_scope local_scopes = let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let notation_binder_source_eq s1 s2 = match s1, s2 with - | NtnParsedAsConstr, NtnParsedAsConstr -> true - | NtnParsedAsIdent, NtnParsedAsIdent -> true - | NtnParsedAsPattern, NtnParsedAsPattern -> true - | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false +| NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 +| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 +| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true |