first moogle template checkin

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

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 7cf16ee53403f1d908c20984a3834d42f445e514..9695d714b7658940392fc4401af71d3701d7298f 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -41,7 +41,11 @@ let apply_subst_gen ~appl_fun subst term =
   let module S = CicSubstitution in 
    function
       C.Rel _ as t -> t
-    | C.Var _  as t -> t
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+       in
+       C.Var (uri, exp_named_subst')
     | C.Meta (i, l) -> 
         (try
           let t = List.assoc i subst in
@@ -598,7 +602,6 @@ let delift n subst context metasenv l t =
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
 debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
-print_string "\nCicMetaSubst: UNCERTAIN" ;
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)