let sober ?(flatten=false) c t =
if flatten then flatten_appls t else (assert (Ut.is_sober c t); t)
-let alpha_equivalence ?flatten c t1 t2 =
+let alpha ?flatten c t1 t2 =
let t1 = sober ?flatten c t1 in
let t2 = sober ?flatten c t2 in
Ut.alpha_equivalence t1 t2
let occurs c ~what ~where =
let result = ref false in
let equality c t1 t2 =
- let r = alpha_equivalence ~flatten:true c t1 t2 in
+ let r = alpha ~flatten:true c t1 t2 in
result := !result || r; r
in
let context, what, with_what = c, [what], [C.Rel 0] in