Merge PR #12246: Adding support for applying in several hypotheses at the same time (granting #9816)

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

7 files changed, 16 insertions, 16 deletions

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 072206c39c..89a14c7c12 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -407,8 +407,8 @@ GRAMMAR EXTEND Gram
       | -> { [] } ] ]
   ;
   in_hyp_as:
-    [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
-      | -> { None } ] ]
+    [ [ "in"; l = LIST1 [id = id_or_meta; ipat = as_ipat -> { (id,ipat) } ] SEP "," -> { l }
+      | -> { [] } ] ]
   ;
   orient_rw:
     [ [ "->" -> { true }
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index edd56ee0f7..cd7b1f7f28 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -458,8 +458,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
 
   let pr_in_hyp_as prc pr_id = function
-    | None -> mt ()
-    | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+    | (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
 
   let pr_in_clause pr_id = function
     | { onhyps=None; concl_occs=NoOccurrences } ->
@@ -756,7 +755,7 @@ let pr_goal_selector ~toplevel s =
             (if a then mt() else primitive "simple ") ++
               primitive (with_evars ev "apply") ++ spc () ++
               prlist_with_sep pr_comma pr_with_bindings_arg cb ++
-              pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
+              prlist_with_sep spc (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
           )
         | TacElim (ev,cb,cbo) ->
           hov 1 (
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index eaedf8d9c1..7b2c8e1d04 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -108,7 +108,7 @@ type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+      ('nam * 'dtrm intro_pattern_expr CAst.t option) list
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 50767821e4..2382dcfbb9 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -107,7 +107,7 @@ type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+      ('nam * 'dtrm intro_pattern_expr CAst.t option) list
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 47f1d3bf66..871f418915 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -444,11 +444,11 @@ let intern_red_expr ist = function
   | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
 
-let intern_in_hyp_as ist lf (id,ipat) =
-  (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
-
 let intern_hyp_list ist = List.map (intern_hyp ist)
 
+let intern_in_hyp_as ist lf (idl,ipat) =
+  (intern_hyp ist idl, Option.map (intern_intro_pattern lf ist) ipat)
+
 let intern_inversion_strength lf ist = function
   | NonDepInversion (k,idl,ids) ->
       NonDepInversion (k,intern_hyp_list ist idl,
@@ -527,7 +527,7 @@ let rec intern_atomic lf ist x =
       TacIntroPattern (ev,List.map (intern_intro_pattern lf ist) l)
   | TacApply (a,ev,cb,inhyp) ->
       TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
-                Option.map (intern_in_hyp_as ist lf) inhyp)
+                List.map (intern_in_hyp_as ist lf) inhyp)
   | TacElim (ev,cb,cbo) ->
       TacElim (ev,intern_constr_with_bindings_arg ist cb,
                Option.map (intern_constr_with_bindings ist) cbo)
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
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)