apply_subst did not apply the substitution to the explicit named substitution

[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 e7b0e3661387d3b986a292858962532f9c4588a5..d7b52acfaf2ce8918b57fb90384765f46d468fab 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
@@ -504,14 +508,19 @@ let delift n subst context metasenv l t =
                     (*CSC: deliftato la regola per il LetIn                 *)
                     (*CSC: FALSO! La regola per il LetIn non lo fa          *)
          else
-          (match List.nth context (m-k-1) with
-            Some (_,C.Def (t,_)) ->
-             (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
-             (*CSC: first order unification. Does it help or does it harm? *)
-             deliftaux k (S.lift m t)
-          | Some (_,C.Decl t) ->
-             C.Rel ((position (m-k) l) + k)
-          | None -> raise (MetaSubstFailure "RelToHiddenHypothesis"))
+          (try
+            match List.nth context (m-k-1) with
+               Some (_,C.Def (t,_)) ->
+                (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
+                (*CSC: first order unification. Does it help or does it harm? *)
+                deliftaux k (S.lift m t)
+             | Some (_,C.Decl t) ->
+                C.Rel ((position (m-k) l) + k)
+             | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
+           with
+            Failure _ ->
+             raise (MetaSubstFailure "Unbound variable found in deliftaux")
+          )
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst