From ebb2a987b774e92496bde4e161f0c138e7f9b07a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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