X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=4126d04464e6626a1b1a0c4e32389138709cf2d7;hb=756c1e676368d9addc75438bce97a71e34287f18;hp=ce7aa5280a46118ef14c5ceae312a0600132a956;hpb=c169f48a31abaea726adf852081e274fcb67f770;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index ce7aa5280..4126d0446 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -130,7 +130,7 @@ let fo_unif_new metasenv context t1 t2 =
        | (C.Sort _ ,_)
        | (_, C.Sort _)
        | (C.Implicit, _)
-       | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
+       | (_, C.Implicit) -> if R.are_convertible context t1 t2 then subst
                             else raise UnificationFailed
        | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
        | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
@@ -163,7 +163,7 @@ let fo_unif_new metasenv context t1 t2 =
        | (C.MutInd  _, _) 
        | (_, C.MutInd _)
        | (C.MutConstruct _, _)
-       | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
+       | (_, C.MutConstruct _) -> if R.are_convertible context t1 t2 then subst
                                    else raise UnificationFailed
        | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
                       let subst' = fo_unif_aux subst k outt1 outt2 in
@@ -172,7 +172,7 @@ let fo_unif_new metasenv context t1 t2 =
        | (C.Fix _, _)
        | (_, C.Fix _) 
        | (C.CoFix _, _)
-       | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
+       | (_, C.CoFix _) -> if R.are_convertible context t1 t2 then subst
                            else raise UnificationFailed
        | (_,_) -> raise UnificationFailed
    in fo_unif_aux [] 0 t1 t2;;