added to CicMetaSubst subst wrapper for CicReduction.are_convertible

[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 50387922d184e9d217c93a70c0a188e1aeeb5646..e0ec5cb447d0c30d43ac5fd1cd883b1c24b098d7 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -51,7 +51,7 @@ let type_of_aux' metasenv subst context term =
 
 let rec fo_unif_subst subst context metasenv t1 t2 =  
  let module C = Cic in
- let module R = CicReduction in
+ let module R = CicMetaSubst in
  let module S = CicSubstitution in
   match (t1, t2) with
      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
@@ -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 context t1' t2'
+                R.are_convertible subst context t1' t2'
          ) true ln lm
        in
         if ok then
@@ -165,14 +165,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 context t1 t2 then
+       if R.are_convertible 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 context t1 t2 then
+       if R.are_convertible subst context t1 t2 then
         subst, metasenv
        else
         raise (UnificationFailure (sprintf