| B.GRef (a, uri) ->
let f = function
| _, _, B.Abbr v when delta ->
- P.add ~gdelta:1 ();
- step f ~delta ~rt m v
- | _, _, B.Abst w when rt ->
- P.add ~grt:1 ();
- step f ~delta ~rt m w
+ P.add ~gdelta:1 (); step f ~delta ~rt m v
+ | _, _, B.Abst w when rt ->
+ P.add ~grt:1 (); step f ~delta ~rt m w
+ | _, _, B.Void ->
+ assert false
| e, _, b ->
f m (Some (e, b)) x
in
P.add ~lrt:1 ();
step f ~delta ~rt {m with c = c} w
| B.Void ->
- f {m with c = c} None x
+ assert false
| b ->
let f e = f {m with c = c} (Some (e, b)) x in
B.apix C.err f a
if r then begin L.unbox level; f () end else error3 mw.c v w u
in
let g r = if r then f r else ac f ~si true mu u mw w in
- if S.eq mu mw then are_alpha_convertible g u w else g false
+(* if S.eq mu mw then are_alpha_convertible g u w else *) g false
in
if rt then domain f mw u else f mw u
projects / helm.git / commitdiff
