From e22add7d893bdc52bc123c671e839ce8eeabd3c4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 28 Mar 2018 15:27:23 +0200 Subject: Glob_ops: cosmetic renaming to reflect the type of objects. --- pretyping/glob_ops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/glob_ops.ml') 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 -- cgit v1.2.3