added to CicMetaSubst subst wrapper for CicReduction.are_convertible

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 04cf03c67b81f4b70eafd229694b71ffec9b162d..f8a73f2f53b0fd4e00cfb3e73f4d832def6a2fd3 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -483,6 +483,11 @@ let whd subst context term =
     raise (MetaSubstFailure ("Weak head reduction failure: " ^
       Printexc.to_string e))
 
+let are_convertible subst context t1 t2 =
+  let context = apply_subst_context subst context in
+  let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in
+  CicReduction.are_convertible context t1 t2
+
 let type_of_aux' metasenv subst context term =
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index 3d1032aa85b629092ea3b4ca6f8a4a90aeb77506..635825c7f34c696116a8bd23bb4451c74550de3f 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -69,6 +69,10 @@ val ppsubst: substitution -> string
  * the calculus *)
 
 val whd: substitution -> Cic.context -> Cic.term -> Cic.term
+val are_convertible:
+  substitution -> Cic.context -> Cic.term -> Cic.term ->
+    bool
 val type_of_aux':
-  Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
+  Cic.metasenv -> substitution -> Cic.context -> Cic.term ->
+    Cic.term
 

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