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 /pretyping/patternops.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 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index d784fc0ed6..c1e91ca2f5 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -39,11 +39,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PSoApp (id1, arg1), PSoApp (id2, arg2) -> Id.equal id1 id2 && List.equal constr_pattern_eq arg1 arg2 | PLambda (v1, t1, b1), PLambda (v2, t2, b2) -> - name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PProd (v1, t1, b1), PProd (v2, t2, b2) -> - name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) -> - name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 + Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PSort s1, PSort s2 -> glob_sort_eq s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> @@ -73,7 +73,7 @@ and cofixpoint_eq (i1, r1) (i2, r2) = rec_declaration_eq r1 r2 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = - Array.equal name_eq n1 n2 && + Array.equal Name.equal n1 n2 && Array.equal eq_constr c1 c2 && Array.equal eq_constr r1 r2 |