- Procedural convertible rewrites in the conclusion are now detected and replaced...

[helm.git] / helm / software / components / acic_procedural / proceduralHelpers.ml

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index c42fe753212b780c382f6b5d647e7048cd7c33db..4305f915340941a414ccea26e4ce5a460d88b679 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -239,7 +239,7 @@ let flatten_appls =
 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
@@ -247,7 +247,7 @@ let alpha_equivalence ?flatten c 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