From 460e778b47270838f98f5efd65518c1a31c96e92 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 7 Apr 2009 17:21:41 +0000 Subject: [PATCH] select honors the substitution --- helm/software/components/ng_tactics/nTacStatus.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 1c7029f4a..6240c7430 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -183,8 +183,15 @@ let select_term low_status (name,context,term) (wanted,path) = in aux ctx status t in + let _,_,_,subst,_ = low_status.pstatus in let rec select status ctx pat cic = match pat, cic with + | _, NCic.Meta (i,lc) when List.mem_assoc i subst -> + let cic = + let _,_,t,_ = NCicUtils.lookup_subst i subst in + NCicSubstitution.subst_meta lc t + in + select status ctx pat cic | NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) -> let status, t = select status ctx t1 t2 in let status, s = select status ctx s1 s2 in @@ -230,7 +237,8 @@ let select_term low_status (name,context,term) (wanted,path) = | NCic.Implicit _, t -> status, t | _,t -> fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[] - ~context:[] ~subst:[] pat)) + ~context:[] ~subst:[] pat ^ " against " ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t)) in let status, term = select low_status context path term in let term = (name, context, term) in -- 2.39.2