select honors the substitution

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 1c7029f4ab038e8fb7e4f9fa6e06c043e9732ea1..6240c74309447a5036c3ec225250aff942fe6c8b 100644 (file)
--- 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