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.

---
 user-contrib/Ltac2/tac2tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 9ca38d64df..69758b3f37 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -106,7 +106,7 @@ let apply adv ev cb cl =
   | None -> Tactics.apply_with_delayed_bindings_gen adv ev cb
   | Some (id, cl) ->
     let cl = Option.map mk_intro_pattern cl in
-    Tactics.apply_delayed_in adv ev id cb cl
+    Tactics.apply_delayed_in adv ev id cb cl Tacticals.New.tclIDTAC
 
 let mk_destruction_arg = function
 | ElimOnConstr c ->
-- 
cgit v1.2.3