From efecceaaba8fc1fc447ce502ef64ac8d66544a0d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Apr 2020 22:12:20 +0200
Subject: Granting #9816: apply in takes several hypotheses.

---
 plugins/ltac/tacsubst.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac/tacsubst.ml')

diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index ec44ae4698..5f09666778 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -128,7 +128,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
   | TacIntroPattern (ev,l) -> TacIntroPattern (ev,List.map (subst_intro_pattern subst) l)
   | TacApply (a,ev,cb,cl) ->
-      TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
+      TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,
+                List.map (on_snd (Option.map (subst_intro_pattern subst))) cl)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,subst_glob_with_bindings_arg subst cb,
                Option.map (subst_glob_with_bindings subst) cbo)
-- 
cgit v1.2.3