diff options
| author | ppedrot | 2012-12-18 18:52:54 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-18 18:52:54 +0000 |
| commit | c3ca134628ad4d9ef70a13b65c48ff17c737238f (patch) | |
| tree | 136b4efbc3aefe76dcd2fa772141c774343f46df /interp/constrexpr_ops.ml | |
| parent | 6946bbbf2390024b3ded7654814104e709cce755 (diff) | |
Modulification of name
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index e9dae6421b..28faa2ce6a 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -109,7 +109,7 @@ let rec constr_expr_eq e1 e2 = List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) -> - name_eq na1 na2 && + Name.equal na1 na2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) -> @@ -132,14 +132,14 @@ let rec constr_expr_eq e1 e2 = List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 | CLetTuple (_, n1, (m1, e1), t1, b1), CLetTuple (_, n2, (m2, e2), t2, b2) -> - List.equal (eq_located name_eq) n1 n2 && - Option.equal (eq_located name_eq) m1 m2 && + List.equal (eq_located Name.equal) n1 n2 && + Option.equal (eq_located Name.equal) m1 m2 && Option.equal constr_expr_eq e1 e2 && constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CIf (_, e1, (n1, r1), t1, f1), CIf (_, e2, (n2, r2), t2, f2) -> constr_expr_eq e1 e2 && - Option.equal (eq_located name_eq) n1 n2 && + Option.equal (eq_located Name.equal) n1 n2 && Option.equal constr_expr_eq r1 r2 && constr_expr_eq t1 t2 && constr_expr_eq f1 f2 @@ -176,7 +176,7 @@ and args_eq (a1,e1) (a2,e2) = and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) = constr_expr_eq e1 e2 && - Option.equal (eq_located name_eq) n1 n2 && + Option.equal (eq_located Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq (_, p1, e1) (_, p2, e2) = @@ -185,7 +185,7 @@ and branch_expr_eq (_, p1, e1) (_, p2, e2) = and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) = (** Don't care about the [binder_kind] *) - List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2 + List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = (eq_located Id.equal id1 id2) && @@ -210,10 +210,10 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with and local_binder_eq l1 l2 = match l1, l2 with | LocalRawDef (n1, e1), LocalRawDef (n2, e2) -> - eq_located name_eq n1 n2 && constr_expr_eq e1 e2 + eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 | LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) - List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2 + List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = |