X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=4305f915340941a414ccea26e4ce5a460d88b679;hb=0ef9250d71eacd6b1022194128e6acfb74d52aac;hp=c42fe753212b780c382f6b5d647e7048cd7c33db;hpb=cdd3fc617825db73ce08a0cb700e2a8e115b4fb3;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index c42fe7532..4305f9153 100644
--- 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