- and aux_rev c2 r2 c1 r1 = aux c1 r1 c2 r2 in
- let f c1' r1 = whd (aux c1' r1) c2 t2 in
- whd f c1 t1
-
-and are_convertible_stacks f c1 c2 =
- let map f v1 v2 = are_convertible f c1 v1 c2 v2 in
- if List.length c1.s <> List.length c2.s then f false else
- C.forall2 f map c1.s c2.s
-
-let are_convertible f c t1 t2 = are_convertible f c t1 c t2
-
-let rec ho_whd f c t =
- let aux c' = function
- | Sort_ h -> f c' (Sort h)
- | Bind_ (w, t) -> f c' (Abst w)
- | LRef_ (_, Some w) -> ho_whd f c w
- | GRef_ (_, B.Abst u) -> ho_whd f c u
- | GRef_ (_, B.Abbr u) -> ho_whd f c u
- | LRef_ (_, None) -> assert false
- | GRef_ (_, B.Void) -> assert false
- in
- whd aux c t
-
-let push f c b =
- assert (c.l = empty_e && c.s = []);
- let f g = f {c with g = g} in
- push_e f b c.g
-
-let get f c i =
- let gl, ge = c.g in
- if i >= gl then error i;
- f (List.nth ge (gl - (succ i)))
-
-let empty_context = {
- g = empty_e; l = empty_e; s = []
-}
-
-let iter f map c =
- let _, ge = c.g in
- C.list_iter f map ge
+ and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
+ let f m1 r1 = whd (aux m1 r1) c2 m2 t2 in
+ whd f c1 m1 t1
+
+and are_convertible_stacks f c1 m1 c2 m2 =
+ let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in
+ let map f v1 v2 = are_convertible f c1 mm1 v1 c2 mm2 v2 in
+ if List.length m1.s <> List.length m2.s then f false else
+ C.forall2 f map m1.s m2.s
+
+let are_convertible f c t1 t2 =
+ L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2);
+ are_convertible f c empty_machine t1 c empty_machine t2