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/tacinterp.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 3d734d3a66..db86567114 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1667,10 +1667,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
             (k,(make ?loc f))) cb
         in
         let sigma,tac = match cl with
-          | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
-          | Some cl ->
-              let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in
-              sigma, Tactics.apply_delayed_in a ev id l cl in
+          | [] -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
+          | cl ->
+              let sigma,cl = List.fold_left_map (interp_in_hyp_as ist env) sigma cl in
+              sigma, List.fold_right (fun (id,ipat) -> Tactics.apply_delayed_in a ev id l ipat) cl Tacticals.New.tclIDTAC in
         Tacticals.New.tclWITHHOLES ev tac sigma
       end
       end
-- 
cgit v1.2.3