- occur check test anticipated to the delift phase

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index e0ec5cb447d0c30d43ac5fd1cd883b1c24b098d7..704eecb467135939170c631c373236c36c3ffb00 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -66,7 +66,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
                 (* First possibility:  restriction    *)
                 (* Second possibility: unification    *)
                 (* Third possibility:  convertibility *)
-                R.are_convertible subst context t1' t2'
+                R.are_convertible metasenv subst context t1' t2'
          ) true ln lm
        in
         if ok then
@@ -85,11 +85,10 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
          let lifted_oldt = S.lift_meta l oldt in
           fo_unif_subst subst context metasenv lifted_oldt t
         with Not_found ->
-         let t',metasenv' = CicMetaSubst.delift context metasenv l t in
+         let t',metasenv' = CicMetaSubst.delift n subst context metasenv l t in
           (n, t')::subst, metasenv'
        in
-        let (_,_,meta_type) = 
-         List.find (function (m,_,_) -> m=n) metasenv' in
+        let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
         let tyt = type_of_aux' metasenv' subst' context t in
          fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
@@ -165,14 +164,14 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
    | (C.Fix _, _) | (_, C.Fix _) 
    | (C.CoFix _, _) | (_, C.CoFix _) -> 
-       if R.are_convertible subst context t1 t2 then
+       if R.are_convertible metasenv subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf
           "Can't unify %s with %s because they are not convertible"
           (CicPp.ppterm t1) (CicPp.ppterm t2)))
    | (_,_) ->
-       if R.are_convertible subst context t1 t2 then
+       if R.are_convertible metasenv subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf