From ebb2a987b774e92496bde4e161f0c138e7f9b07a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Mar 2004 16:42:29 +0000
Subject: [PATCH] apply_subst did not apply the substitution to the explicit
 named substitution (local context) of a variable.

---
 helm/ocaml/cic_unification/cicMetaSubst.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 7cf16ee53..d7b52acfa 100644
--- 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
-- 
2.39.2