diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-28 15:27:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-28 20:50:20 +0200 |
| commit | e22add7d893bdc52bc123c671e839ce8eeabd3c4 (patch) | |
| tree | 620eb0c43445a9541d2806176012d20f508cfd2f /pretyping/glob_ops.ml | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Glob_ops: cosmetic renaming to reflect the type of objects.
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 74f2cefab..e89bbf7c3 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> f m1 m2 && Name.equal pat1 pat2 && Option.equal f p1 p2 && f c1 c2 && f t1 t2 - | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> + | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) -> fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 |