diff options
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 4b1af9147c..011c4a6e4e 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -16,6 +16,7 @@ open Libnames open Namegen open Glob_term open Constrexpr +open Notation open Decl_kinds (***********************) @@ -80,7 +81,7 @@ let rec cases_pattern_expr_eq p1 p2 = | CPatOr a1, CPatOr a2 -> List.equal cases_pattern_expr_eq a1 a2 | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> - String.equal n1 n2 && + notation_eq n1 n2 && cases_pattern_notation_substitution_eq s1 s2 && List.equal cases_pattern_expr_eq l1 l2 | CPatPrim i1, CPatPrim i2 -> @@ -165,7 +166,7 @@ let rec constr_expr_eq e1 e2 = | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(n1, s1), CNotation(n2, s2) -> - String.equal n1 n2 && + notation_eq n1 n2 && constr_notation_substitution_eq s1 s2 | CPrim i1, CPrim i2 -> prim_token_eq i1 i2 |