- new implementation of the apply case in fo_unif using beta expansion

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

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e8ea0769de76416d369ba4d5f5b9ff63ee0ed945..7bd3de5c2a0f09aa92e0094d80f999dac7272276 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -452,6 +452,7 @@ and type_of_aux' metasenv context t =
     | ((uri,t) as subst)::tl ->
        let typeofvar =
         CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: why was this code here? it is wrong
        (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
@@ -463,16 +464,19 @@ and type_of_aux' metasenv context t =
             (RefineFailure
              ("Unkown variable definition " ^ UriManager.string_of_uri uri))
        ) ;
+*)
        let typeoft,metasubst',metasenv' =
         type_of_aux metasubst metasenv context t
        in
-        try
-         let metasubst'',metasenv'' =
+        let metasubst'',metasenv'' =
+         try
           fo_unif_subst metasubst' context metasenv' typeoft typeofvar
-         in
-          check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
-        with _ ->
-         raise (RefineFailure "Wrong Explicit Named Substitution")
+         with _ ->
+          raise (RefineFailure
+           ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
+            " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
+        in
+         check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
   in
    check_exp_named_subst_aux metasubst metasenv []