- let map f t (a, l, b) = f (Z.Bind (a, l, b, t)) in
+ let map f t (y, l, b) = f (Z.Bind (y, l, b, t)) in
get f c m i
| Z.Cast (_, t) -> whd f c m t
| Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t
get f c m i
| Z.Cast (_, t) -> whd f c m t
| Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t
- | Z.Bind (a, l, Z.Abst w, t) ->
+ | Z.Bind (y, l, Z.Abst w, t) ->
- | [] -> f m (Bind_ (a, l, w, t))
+ | [] -> f m (Bind_ (y, l, w, t))
- | Z.Bind (a, l, b, t) ->
+ | Z.Bind (y, l, b, t) ->
ho_whd f c empty_machine t
let rec are_convertible f st a c m1 t1 m2 t2 =
(* L.warn "entering R.are_convertible"; *)
let rec aux m1 r1 m2 r2 =
(* L.warn "entering R.are_convertible_aux"; *)
ho_whd f c empty_machine t
let rec are_convertible f st a c m1 t1 m2 t2 =
(* L.warn "entering R.are_convertible"; *)
let rec aux m1 r1 m2 r2 =
(* L.warn "entering R.are_convertible_aux"; *)
- | Sort_ h1, Sort_ h2 ->
- if h1 = h2 then f a else f false
- | LRef_ (i1, _), LRef_ (i2, _) ->
+ | Sort_ k1, Sort_ k2 ->
+ if k1 = k2 then f a else f false
+ | LRef_ (i1, _), LRef_ (i2, _) ->
if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false
| GRef_ (_, {E.n_apix = a1}, _, E.Abst _),
if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false
| GRef_ (_, {E.n_apix = a1}, _, E.Abst _),
- GRef_ (_, {E.n_apix = a2}, _, E.Abst _) ->
+ GRef_ (_, {E.n_apix = a2}, _, E.Abst _) ->
if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
| GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1),
if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
| GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1),
- GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) ->
+ GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) ->
- | _, GRef_ (_, _, _, E.Abbr v2) ->
+ | _, GRef_ (_, _, _, E.Abbr v2) ->
- | GRef_ (_, _, _, E.Abbr v1), _ ->
+ | GRef_ (_, _, _, E.Abbr v1), _ ->
- | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) ->
+ | Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) ->
let l = P.new_mark () in
let h c =
let m1, m2 = inc m1, inc m2 in
let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in
ZS.subst f l l1 t1
in
let l = P.new_mark () in
let h c =
let m1, m2 = inc m1, inc m2 in
let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in
ZS.subst f l l1 t1
in
are_convertible f st a c m1 w1 m2 w2
(* we detect the AUT-QE reduction rule for type/prop inclusion *)
are_convertible f st a c m1 w1 m2 w2
(* we detect the AUT-QE reduction rule for type/prop inclusion *)
- | Sort_ _, Bind_ (a2, l2, w2, t2) when !G.si ->
+ | Sort_ _, Bind_ (y2, l2, w2, t2) when !G.si ->
let m1, m2 = inc m1, inc m2 in
let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in
let m1, m2 = inc m1, inc m2 in
let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in
and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
let g m1 r1 = whd (aux m1 r1) c m2 t2 in
if a = false then f false else whd g c m1 t1
and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
let g m1 r1 = whd (aux m1 r1) c m2 t2 in
if a = false then f false else whd g c m1 t1