From: Claudio Sacerdoti Coen Date: Fri, 5 Mar 2004 16:42:29 +0000 (+0000) Subject: apply_subst did not apply the substitution to the explicit named substitution X-Git-Tag: v0_0_4~40 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ebb2a987b774e92496bde4e161f0c138e7f9b07a;p=helm.git apply_subst did not apply the substitution to the explicit named substitution (local context) of a variable. --- 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