From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 22 Jan 2004 12:22:34 +0000 (+0000)
Subject: added to CicMetaSubst subst wrapper for CicReduction.are_convertible
X-Git-Tag: V_0_5_1_4~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6696898978f86977863429cc3a8690d2546a918b;p=helm.git

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 04cf03c67..f8a73f2f5 100644
--- 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 3d1032aa8..635825c7f 100644
--- 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 50387922d..e0ec5cb44 100644
--- 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