Adding a new intro-pattern for "apply in" on the fly. Using syntax

"pat/term" for "apply term on current_hyp as pat".

11 files changed, 208 insertions, 187 deletions

diff --git a/tactics/elim.mli b/tactics/elim.mli
index b5e89de081..df75f8ba5b 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -14,7 +14,7 @@ open Misctypes
 (** Eliminations tactics. *)
 
 val introCaseAssumsThen :
-  (intro_pattern_expr Loc.located list -> branch_assumptions -> unit Proofview.tactic) ->
+  (Tacexpr.intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic
 
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 4899cd91d5..9008af77b8 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -77,9 +77,9 @@ val discrHyp     : Id.t -> unit Proofview.tactic
 val discrEverywhere : evars_flag -> unit Proofview.tactic
 val discr_tac    : evars_flag ->
   constr with_bindings induction_arg option -> unit Proofview.tactic
-val inj          : intro_pattern_expr Loc.located list option -> evars_flag ->
+val inj          : intro_patterns option -> evars_flag ->
   clear_flag -> constr with_bindings -> unit Proofview.tactic
-val injClause    : intro_pattern_expr Loc.located list option -> evars_flag ->
+val injClause    : intro_patterns option -> evars_flag ->
   constr with_bindings induction_arg option -> unit Proofview.tactic
 val injHyp       : clear_flag -> Id.t -> unit Proofview.tactic
 val injConcl     : unit Proofview.tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 089fef4bc9..49a5bcd7ea 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -396,6 +396,8 @@ let rec get_names allow_conj (loc,pat) = match pat with
       error "Injection patterns not allowed for inversion equations."
   | IntroAction (IntroOrAndPattern l) ->
       error "Disjunctive patterns not allowed for inversion equations."
+  | IntroAction (IntroApplyOn (c,pat)) ->
+      error "Apply patterns not allowed for inversion equations."
   | IntroNaming (IntroIdentifier id) ->
       (Some id,[id])
 
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 7416d29bb1..a71b5eeb3a 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -15,14 +15,14 @@ open Tacexpr
 type inversion_status = Dep of constr option | NoDep
 
 val inv_clause :
-  inversion_kind -> or_and_intro_pattern_expr located option -> Id.t list ->
+  inversion_kind -> constr or_and_intro_pattern_expr located option -> Id.t list ->
     quantified_hypothesis -> unit Proofview.tactic
 
-val inv : inversion_kind -> or_and_intro_pattern_expr located option ->
+val inv : inversion_kind -> constr or_and_intro_pattern_expr located option ->
   quantified_hypothesis -> unit Proofview.tactic
 
 val dinv : inversion_kind -> constr option ->
-  or_and_intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
+  constr or_and_intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
 
 val inv_tac : Id.t -> unit Proofview.tactic
 val inv_clear_tac : Id.t -> unit Proofview.tactic
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index f2b3b225b5..629a218e58 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -50,7 +50,10 @@ val coerce_to_constr_context : Value.t -> constr
 
 val coerce_to_ident : bool -> Environ.env -> Value.t -> Id.t
 
-val coerce_to_intro_pattern : Environ.env -> Value.t -> intro_pattern_expr
+val coerce_to_intro_pattern : Environ.env -> Value.t -> constr intro_pattern_expr
+
+val coerce_to_intro_pattern_naming :
+  Environ.env -> Value.t -> intro_pattern_naming_expr
 
 val coerce_to_intro_pattern_naming :
   Environ.env -> Value.t -> intro_pattern_naming_expr
@@ -71,7 +74,7 @@ val coerce_to_evaluable_ref :
 val coerce_to_constr_list : Environ.env -> Value.t -> constr list
 
 val coerce_to_intro_pattern_list :
-  Loc.t -> Environ.env -> Value.t -> intro_pattern_expr Loc.located list
+  Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns
 
 val coerce_to_hyp : Environ.env -> Value.t -> Id.t
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 0d086d842d..cf8cda014d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -215,36 +215,6 @@ let intern_message_token ist = function
 
 let intern_message ist = List.map (intern_message_token ist)
 
-let rec intern_intro_pattern lf ist = function
-  | loc, IntroNaming pat ->
-      loc, IntroNaming (intern_intro_pattern_naming lf ist pat)
-  | loc, IntroAction pat ->
-      loc, IntroAction (intern_intro_pattern_action lf ist pat)
-  | loc, IntroForthcoming _ as x -> x
-
-and intern_intro_pattern_naming lf ist = function
-  | IntroIdentifier id ->
-      IntroIdentifier (intern_ident lf ist id)
-  | IntroFresh id ->
-      IntroFresh (intern_ident lf ist id)
-  | IntroWildcard | IntroAnonymous as x -> x
-
-and intern_intro_pattern_action lf ist = function
-  | IntroOrAndPattern l ->
-      IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
-  | IntroInjection l ->
-      IntroInjection (List.map (intern_intro_pattern lf ist) l)
-  | IntroRewrite _ as x -> x
-
-and intern_or_and_intro_pattern lf ist =
-  List.map (List.map (intern_intro_pattern lf ist))
-
-let intern_or_and_intro_pattern_loc lf ist (loc,l) =
-  (loc,intern_or_and_intro_pattern lf ist l)
-
-let intern_intro_pattern_naming_loc lf ist (loc,pat) =
-  (loc,intern_intro_pattern_naming lf ist pat)
-
 let intern_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
@@ -287,6 +257,38 @@ let intern_constr_with_bindings ist (c,bl) =
 let intern_constr_with_bindings_arg ist (clear,c) =
   (clear,intern_constr_with_bindings ist c)
 
+let rec intern_intro_pattern lf ist = function
+  | loc, IntroNaming pat ->
+      loc, IntroNaming (intern_intro_pattern_naming lf ist pat)
+  | loc, IntroAction pat ->
+      loc, IntroAction (intern_intro_pattern_action lf ist pat)
+  | loc, IntroForthcoming _ as x -> x
+
+and intern_intro_pattern_naming lf ist = function
+  | IntroIdentifier id ->
+      IntroIdentifier (intern_ident lf ist id)
+  | IntroFresh id ->
+      IntroFresh (intern_ident lf ist id)
+  | IntroWildcard | IntroAnonymous as x -> x
+
+and intern_intro_pattern_action lf ist = function
+  | IntroOrAndPattern l ->
+      IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
+  | IntroInjection l ->
+      IntroInjection (List.map (intern_intro_pattern lf ist) l)
+  | IntroRewrite _ as x -> x
+  | IntroApplyOn (c,pat) ->
+      IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
+
+and intern_or_and_intro_pattern lf ist =
+  List.map (List.map (intern_intro_pattern lf ist))
+
+let intern_or_and_intro_pattern_loc lf ist (loc,l) =
+  (loc,intern_or_and_intro_pattern lf ist l)
+
+let intern_intro_pattern_naming_loc lf ist (loc,pat) =
+  (loc,intern_intro_pattern_naming lf ist pat)
+
   (* TODO: catch ltac vars *)
 let intern_induction_arg ist = function
   | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d9963a615d..026ed94a4c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -425,6 +425,7 @@ let rec intropattern_ids (loc,pat) = match pat with
       List.flatten (List.map intropattern_ids (List.flatten ll))
   | IntroAction (IntroInjection l) ->
       List.flatten (List.map intropattern_ids l)
+  | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat
   | IntroNaming (IntroWildcard | IntroAnonymous | IntroFresh _)
   | IntroAction (IntroRewrite _)
   | IntroForthcoming _ -> []
@@ -724,7 +725,7 @@ let rec message_of_value env v =
   else if has_type v (topwit wit_unit) then str "()"
   else if has_type v (topwit wit_int) then int (out_gen (topwit wit_int) v)
   else if has_type v (topwit wit_intro_pattern) then
-    Miscprint.pr_intro_pattern (out_gen (topwit wit_intro_pattern) v)
+    Miscprint.pr_intro_pattern (pr_constr_env env) (out_gen (topwit wit_intro_pattern) v)
   else if has_type v (topwit wit_constr_context) then
     pr_constr_env env (out_gen (topwit wit_constr_context) v)
   else match Value.to_list v with
@@ -752,49 +753,69 @@ let interp_message ist gl l =
      are raised now and not at printing time *)
   prlist_with_sep spc (interp_message_token ist gl) l
 
-let rec interp_intro_pattern ist env = function
+let rec interp_intro_pattern ist env sigma = function
   | loc, IntroAction pat ->
-      loc, IntroAction (interp_intro_pattern_action ist env pat)
+      let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in
+      sigma, (loc, IntroAction pat)
   | loc, IntroNaming (IntroIdentifier id) ->
-      loc, interp_intro_pattern_var loc ist env id
+      sigma, (loc, interp_intro_pattern_var loc ist env id)
   | loc, IntroNaming pat ->
-      loc, IntroNaming (snd (interp_intro_pattern_naming ist env (loc,pat)))
-  | loc, IntroForthcoming _  as x -> x
+      sigma, (loc, IntroNaming (interp_intro_pattern_naming loc ist env pat))
+  | loc, IntroForthcoming _  as x -> sigma, x
 
-and interp_intro_pattern_naming ist env = function
-  | loc,IntroFresh id -> loc,IntroFresh (interp_fresh_ident ist env id)
-  | loc,IntroIdentifier id -> loc,interp_intro_pattern_naming_var loc ist env id
-  | loc,(IntroWildcard | IntroAnonymous) as x -> x
+and interp_intro_pattern_naming loc ist env = function
+  | IntroFresh id -> IntroFresh (interp_fresh_ident ist env id)
+  | IntroIdentifier id -> interp_intro_pattern_naming_var loc ist env id
+  | (IntroWildcard | IntroAnonymous) as x -> x
 
-and interp_intro_pattern_action ist env = function
+and interp_intro_pattern_action ist env sigma = function
   | IntroOrAndPattern l ->
-      IntroOrAndPattern (interp_or_and_intro_pattern ist env l)
+      let (sigma,l) = interp_or_and_intro_pattern ist env sigma l in
+      sigma, IntroOrAndPattern l
   | IntroInjection l ->
-      IntroInjection (interp_intro_pattern_list_as_list ist env l)
-  | IntroRewrite _ as x -> x
-
-and interp_or_and_intro_pattern ist env =
-  List.map (interp_intro_pattern_list_as_list ist env)
-
-and interp_intro_pattern_list_as_list ist env = function
+      let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
+      sigma, IntroInjection l
+  | IntroApplyOn (c,ipat) ->
+      let sigma,c = interp_constr ist env sigma c in
+      let sigma,ipat = interp_intro_pattern ist env sigma ipat in
+      sigma, IntroApplyOn (c,ipat)
+  | IntroRewrite _ as x -> sigma, x
+
+and interp_or_and_intro_pattern ist env sigma =
+  List.fold_map (interp_intro_pattern_list_as_list ist env) sigma
+
+and interp_intro_pattern_list_as_list ist env sigma = function
   | [loc,IntroNaming (IntroIdentifier id)] as l ->
-      (try coerce_to_intro_pattern_list loc env (Id.Map.find id ist.lfun)
+      (try sigma, coerce_to_intro_pattern_list loc env (Id.Map.find id ist.lfun)
        with Not_found | CannotCoerceTo _ ->
-	List.map (interp_intro_pattern ist env) l)
-  | l -> List.map (interp_intro_pattern ist env) l
-
-let interp_or_and_intro_pattern_loc ist env (loc,l) =
-  match l with
-  | [[loc',IntroNaming (IntroIdentifier id)]] when (* Hack, see g_tactic.ml4 *) loc' = dloc ->
-      (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with
-       | IntroAction (IntroOrAndPattern l) -> (loc,l)
-       | _ ->
-       raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern"))
-  | l ->
-      (loc,interp_or_and_intro_pattern ist env l)
-
-let interp_in_hyp_as ist env (clear,id,ipat) =
-  (clear,interp_hyp ist env id,Option.map (interp_intro_pattern ist env) ipat)
+         List.fold_map (interp_intro_pattern ist env) sigma l)
+  | l -> List.fold_map (interp_intro_pattern ist env) sigma l
+
+let interp_intro_pattern_naming_option ist env = function
+  | None -> None
+  | Some (loc,pat) -> Some (loc, interp_intro_pattern_naming loc ist env pat)
+
+let interp_or_and_intro_pattern_option ist env sigma = function
+  | None -> sigma, None
+  | Some (loc,l) ->
+      let sigma, l = match l with
+      | [[loc',IntroNaming (IntroIdentifier id)]] when (* Hack, see g_tactic.ml4 *) loc' = dloc ->
+        (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with
+        | IntroAction (IntroOrAndPattern l) -> sigma, l
+        | _ ->
+          raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern"))
+      | l -> interp_or_and_intro_pattern ist env sigma l in
+      sigma, Some (loc,l)
+
+let interp_intro_pattern_option ist env sigma = function
+  | None -> sigma, None
+  | Some ipat ->
+      let sigma, ipat = interp_intro_pattern ist env sigma ipat in
+      sigma, Some ipat
+
+let interp_in_hyp_as ist env sigma (clear,id,ipat) =
+  let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
+  sigma,(clear,interp_hyp ist env id,ipat)
 
 let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
@@ -1691,8 +1712,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacIntroPattern l ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
-        let patterns = interp_intro_pattern_list_as_list ist env l in
-        Tactics.intros_patterns patterns
+        let sigma = Proofview.Goal.sigma gl in
+        let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
+        Tacticals.New.tclWITHHOLES false Tactics.intros_patterns sigma l'
       end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.raw_enter begin fun gl ->
@@ -1715,15 +1737,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma, l =
           List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb
         in
-        let tac = match cl with
-          | None -> fun l -> Tactics.apply_with_bindings_gen a ev l
+        let sigma,tac = match cl with
+          | None -> sigma, fun l -> Tactics.apply_with_bindings_gen a ev l
           | Some cl ->
-              (fun l ->
-                Proofview.Goal.raw_enter begin fun gl ->
-                  let env = Proofview.Goal.env gl in
-                  let (clear,id,cl) = interp_in_hyp_as ist env cl in
-                  Tactics.apply_in a ev clear id l cl
-                end) in
+              let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in
+              sigma, fun l -> Tactics.apply_in a ev clear id l cl in
         Tacticals.New.tclWITHHOLES ev tac sigma l
       end
   | TacElim (ev,(keep,cb),cbo) ->
@@ -1786,11 +1804,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,c) = 
           (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
         in
-        let patt = interp_intro_pattern ist env in
-        Tacticals.New.tclTHEN
-          (Proofview.V82.tclEVARS sigma)
-          (Tactics.forward b (Option.map (interp_tactic ist) t)
-              (Option.map patt ipat) c)
+        let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
+        let tac = Option.map (interp_tactic ist) t in
+        Tacticals.New.tclWITHHOLES false (Tactics.forward b tac ipat) sigma c
       end
   | TacGeneralize cl ->
       let tac arg = Proofview.V82.tactic (Tactics.Simple.generalize_gen arg) in
@@ -1809,7 +1825,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let clp = interp_clause ist env clp in
-        let eqpat = Option.map (interp_intro_pattern_naming ist env) eqpat in
+        let eqpat = interp_intro_pattern_naming_option ist env eqpat in
         if Locusops.is_nowhere clp then
         (* We try to fully-typecheck the term *)
           let (sigma,c_interp) =
@@ -1820,9 +1836,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_tac with_eq na c None cl
           in
-	  Tacticals.New.tclTHEN
-	    (Proofview.V82.tclEVARS sigma)
-            (let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
+	  Tacticals.New.tclWITHHOLES false
+            (let_tac b (interp_fresh_name ist env na) c_interp clp)
+            sigma eqpat
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
@@ -1830,8 +1846,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_pat_tac with_eq na c cl
           in
-          let_pat_tac b (interp_fresh_name ist env na)
-            (interp_pure_open_constr ist env sigma c) clp eqpat
+	  Tacticals.New.tclWITHHOLES false
+            (let_pat_tac b (interp_fresh_name ist env na)
+            (interp_pure_open_constr ist env sigma c) clp) sigma eqpat
       end
 
   (* Automation tactics *)
@@ -1859,17 +1876,16 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.V82.nf_evar_goals <*>
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
-        let l =
-          List.map begin fun (c,(ipato,ipats)) ->
+        let sigma = Proofview.Goal.sigma gl in
+        let sigma,l =
+          List.fold_map begin fun sigma (c,(ipato,ipats)) ->
+            (* TODO: move sigma as a side-effect *)
             let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in
-            let interp_intro_pattern1 = interp_intro_pattern_naming ist env in
-            let interp_intro_pattern2 = interp_or_and_intro_pattern_loc ist env in
-            c,
-            (Option.map interp_intro_pattern1 ipato,
-             Option.map interp_intro_pattern2 ipats)
-          end l
+            let ipato = interp_intro_pattern_naming_option ist env ipato in
+            let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in
+            sigma,(c,(ipato,ipats))
+          end sigma l
         in
-        let sigma = Proofview.Goal.sigma gl in
         let sigma,el =
           Option.fold_map (interp_constr_with_bindings ist env) sigma el in
         let interp_clause = interp_clause ist env in
@@ -2004,22 +2020,19 @@ and interp_atomic ist tac : unit Proofview.tactic =
               in
               sigma , Some c_interp
         in
-        let interp_intro_pattern = interp_or_and_intro_pattern_loc ist env in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in
-        Inv.dinv k c_interp
-          (Option.map interp_intro_pattern ids)
-          dqhyps
+        let sigma,ids = interp_or_and_intro_pattern_option ist env sigma ids in
+        Tacticals.New.tclWITHHOLES false (Inv.dinv k c_interp ids) sigma dqhyps
       end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
-        let interp_intro_pattern = interp_or_and_intro_pattern_loc ist env in
+        let sigma = Proofview.Goal.sigma gl in
         let hyps = interp_hyp_list ist env idl in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env hyp in
-        Inv.inv_clause k
-          (Option.map interp_intro_pattern ids)
-          hyps
-          dqhyps
+        let sigma, ids = interp_or_and_intro_pattern_option ist env sigma ids in
+        Tacticals.New.tclWITHHOLES false (Inv.inv_clause k ids hyps)
+          sigma dqhyps
       end
   | TacInversion (InversionUsing (c,idl),hyp) ->
       Proofview.Goal.raw_enter begin fun gl ->
@@ -2118,7 +2131,7 @@ let () =
 let () =
   let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) ref) in
   Geninterp.register_interp0 wit_ref interp;
-  let interp ist gl pat = (project gl, interp_intro_pattern ist (pf_env gl) pat) in
+  let interp ist gl pat = interp_intro_pattern ist (pf_env gl) (project gl) pat in
   Geninterp.register_interp0 wit_intro_pattern interp;
   let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) pat) in
   Geninterp.register_interp0 wit_clause_dft_concl interp;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 8260da9d71..840cd0c05b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -151,7 +151,7 @@ type branch_args = {
   nassums    : int;         (* the number of assumptions to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
                                true=recursive argument, false=constant *)
-  branchnames : intro_pattern_expr Loc.located list}
+  branchnames : constr intro_pattern_expr Loc.located list}
 
 type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ebe1667f24..de2bbbfaee 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -108,7 +108,7 @@ type branch_args = {
   nassums    : int;         (** the number of assumptions to be introduced *)
   branchsign : bool list;   (** the signature of the branch.
                                true=recursive argument, false=constant *)
-  branchnames : intro_pattern_expr located list}
+  branchnames : intro_patterns}
 
 type branch_assumptions = {
   ba        : branch_args;     (** the branch args *)
@@ -117,16 +117,16 @@ type branch_assumptions = {
 (** [check_disjunctive_pattern_size loc pats n] returns an appropriate 
    error message if |pats| <> n *)
 val check_or_and_pattern_size :
-  Loc.t -> or_and_intro_pattern_expr -> int -> unit
+  Loc.t -> constr or_and_intro_pattern_expr -> int -> unit
 
 (** Tolerate "[]" to mean a disjunctive pattern of any length *)
-val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr ->
-  or_and_intro_pattern_expr
+val fix_empty_or_and_pattern : int -> constr or_and_intro_pattern_expr ->
+  constr or_and_intro_pattern_expr
 
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
-  int -> or_and_intro_pattern_expr located option ->
-    intro_pattern_expr located list array
+  int -> constr or_and_intro_pattern_expr located option ->
+    intro_patterns array
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : Id.t -> goal sigma -> sorts_family
@@ -242,11 +242,11 @@ module New : sig
     constr -> unit Proofview.tactic
 
   val case_then_using :
-    or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
+    constr or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
     constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic
 
   val case_nodep_then_using :
-    or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
+    constr or_and_intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) ->
     constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic
 
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4ed8b51143..44043364dd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -821,7 +821,7 @@ let make_naming id t = function
    [Ti] and the first one (resp last one) being [G] whose hypothesis
    [id] is replaced by P using the proof given by [tac] *)
 
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) naming id clenv0 =
+let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) naming id clenv0 tac =
   let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv0 in
   let clenv =
     if with_classes then
@@ -839,10 +839,10 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) nami
     (Proofview.V82.tclEVARS clenv.evd)
     (if sidecond_first then
        Tacticals.New.tclTHENFIRST
-         (assert_before_gen with_clear naming new_hyp_typ) exact_tac
+         (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
      else
        Tacticals.New.tclTHENLAST
-         (assert_after_gen with_clear naming new_hyp_typ) exact_tac)
+         (assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac)
 
 (********************************************)
 (*       Elimination tactics                *)
@@ -1083,6 +1083,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (
     errorlabstrm "general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars None id elimclause''
+    (fun id -> Proofview.tclUNIT ())
   end
 
 let general_elim_clause with_evars flags id c e =
@@ -1325,7 +1326,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
   aux (make_clenv_binding env sigma (d,thm) lbind)
 
 let apply_in_once sidecond_first with_delta with_destruct with_evars naming
-    id (clear_flag,(loc,(d,lbind))) =
+    id (clear_flag,(loc,(d,lbind))) tac =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -1338,9 +1339,11 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     let sigma = Proofview.Goal.sigma gl in
     try
       let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in
-      Tacticals.New.tclTHEN
-        (clenv_refine_in ~sidecond_first with_evars naming id clause)
-        (apply_clear_request clear_flag false c)
+      clenv_refine_in ~sidecond_first with_evars naming id clause
+        (fun id ->
+          Tacticals.New.tclTHEN
+            (apply_clear_request clear_flag false c)
+            (tac id))
     with e when with_destruct ->
       let e = Errors.push e in
       descend_in_conjunctions aux (fun _ -> raise e) c
@@ -1695,6 +1698,17 @@ let rewrite_hyp assert_style l2r id =
         Tacticals.New.tclZEROMSG (str"Cannot find a known equation.")
   end
 
+let rec prepare_naming loc = function
+  | IntroIdentifier id -> NamingMustBe (loc,id)
+  | IntroAnonymous -> NamingAvoid []
+  | IntroFresh id -> NamingBasedOn (id,[])
+  | IntroWildcard ->
+      error "Did you really mind erasing the newly generated hypothesis?"
+
+let do_replace id = function
+  | NamingMustBe (_,id') when Option.equal Id.equal id (Some id') -> true
+  | _ -> false
+
 let rec explicit_intro_names = function
 | (_, IntroForthcoming _) :: l -> explicit_intro_names l
 | (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l
@@ -1702,6 +1716,8 @@ let rec explicit_intro_names = function
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
 | (_, IntroAction (IntroInjection l)) :: l' ->
     explicit_intro_names (l@l')
+| (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
+    explicit_intro_names (pat::l')
 | (_, (IntroNaming (IntroWildcard | IntroAnonymous | IntroFresh _)
      | IntroAction (IntroRewrite _))) :: l ->
      explicit_intro_names l
@@ -1789,6 +1805,27 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
         (* Skip the side conditions of the rewriting step *)
 	(rewrite_hyp style l2r id)
         (tac thin None [])
+  | IntroApplyOn (c,(loc,pat)) ->
+      let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) pat in
+      let clear = do_replace (Some id) naming in
+      Tacticals.New.tclTHENFIRST
+        (* Skip the side conditions of the apply *)
+        (apply_in_once false true true true (Some (clear,naming)) id
+           (None,(Evd.empty,(c,NoBindings))) tac_ipat)
+	(tac thin None [])
+
+and prepare_intros_loc loc dft = function
+  | IntroNaming ipat ->
+      prepare_naming loc ipat,
+      (fun _ -> Proofview.tclUNIT ())
+  | IntroAction ipat ->
+      prepare_naming loc dft,
+      (let tac thin bound =
+        intro_patterns_core true [] [] thin MoveLast bound 0
+          (fun _ l -> clear_wildcards l) in
+      fun id -> intro_pattern_action loc true true ipat [] tac id)
+  | IntroForthcoming _ -> user_err_loc
+      (loc,"",str "Introduction pattern for one hypothesis expected.")
 
 let intro_patterns_bound_to n destopt =
   intro_patterns_core true [] [] [] destopt
@@ -1819,26 +1856,6 @@ let intros_patterns = function
 (*   Forward reasoning    *)
 (**************************)
 
-let rec prepare_naming loc = function
-  | IntroIdentifier id -> NamingMustBe (loc,id)
-  | IntroAnonymous -> NamingAvoid []
-  | IntroFresh id -> NamingBasedOn (id,[])
-  | IntroWildcard ->
-      error "Did you really mind erasing the newly generated hypothesis?"
-
-let rec prepare_intros_loc loc dft = function
-  | IntroNaming ipat ->
-      prepare_naming loc ipat,
-      (fun _ -> Proofview.tclUNIT ())
-  | IntroAction ipat ->
-      prepare_naming loc dft,
-      (let tac thin bound =
-        intro_patterns_core true [] [] thin MoveLast bound 0
-          (fun _ l -> clear_wildcards l) in
-      fun id -> intro_pattern_action loc true true ipat [] tac id)
-  | IntroForthcoming _ -> user_err_loc
-      (loc,"",str "Introduction pattern for one hypothesis expected.")
-
 let prepare_intros dft = function
   | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
   | Some (loc,ipat) -> prepare_intros_loc loc dft ipat
@@ -1851,10 +1868,6 @@ let ipat_of_name = function
    let c = fst (decompose_app ((strip_lam_assum c))) in
    if isVar c then Some (destVar c) else None
 
-let do_replace id = function
-  | NamingMustBe (_,id') when Option.equal Id.equal id (Some id') -> true
-  | _ -> false
-
 let assert_as first ipat c =
   let naming,tac = prepare_intros IntroAnonymous ipat in
   let repl = do_replace (head_ident c) naming in
@@ -1863,39 +1876,27 @@ let assert_as first ipat c =
 
 (* apply in as *)
 
-let as_tac id ipat = match ipat with
-  | Some (loc,IntroAction pat) ->
-      let tac thin bound =
-        intro_patterns_core true [] [] thin MoveLast bound 0
-          (fun _ l -> clear_wildcards l) in
-      intro_pattern_action loc true true pat [] tac id
-  | Some (loc, (IntroNaming _ | IntroForthcoming _)) ->
-      user_err_loc (loc,"",
-                    str "Disjunctive, conjunctive or equality pattern expected")
-  | None -> Proofview.tclUNIT ()
-
-let tclMAPLAST tacfun l =
-  List.fold_right (fun x -> Tacticals.New.tclTHENLAST (tacfun x)) l (Proofview.tclUNIT())
-
-let tclMAPFIRST tacfun l =
-  List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT())
-
 let general_apply_in sidecond_first with_delta with_destruct with_evars
     with_clear id lemmas ipat =
-  let tac (naming,lemma) =
+  let tac (naming,lemma) tac id =
     apply_in_once sidecond_first with_delta with_destruct with_evars
-      naming id lemma in
+      naming id lemma tac in
   let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
   let clear = do_replace (Some id) naming in
-  let lemmas_target =
+  let lemmas_target, last_lemma_target =
     let last,first = List.sep_last lemmas in
-    List.map (fun lem -> (None,lem)) first @ [(Some (clear,naming),last)]
+    List.map (fun lem -> (None,lem)) first, (Some (clear,naming),last)
   in
+  (* We chain apply_in_once, ending with an intro pattern *)
+  List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+
+(*
   if sidecond_first then
     (* Skip the side conditions of the applied lemma *)
     Tacticals.New.tclTHENLAST (tclMAPLAST tac lemmas_target) (ipat_tac id)
   else
     Tacticals.New.tclTHENFIRST (tclMAPFIRST tac lemmas_target) (ipat_tac id)
+*)
 
 let apply_in simple with_evars clear_flag id lemmas ipat =
   general_apply_in false simple simple with_evars clear_flag id lemmas ipat
@@ -2227,7 +2228,7 @@ let check_unused_names names =
   if not (List.is_empty names) && Flags.is_verbose () then
     msg_warning
       (str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
-       ++ str": " ++ prlist_with_sep spc Miscprint.pr_intro_pattern names)
+       ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern Printer.pr_constr) names)
 
 let intropattern_of_name gl avoid = function
   | Anonymous -> IntroNaming IntroAnonymous
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b974f341f1..cee781a8b3 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -102,16 +102,16 @@ val use_clear_hyp_by_default : unit -> bool
 
 (** {6 Introduction tactics with eliminations. } *)
 
-val intro_patterns : intro_pattern_expr located list -> unit Proofview.tactic
-val intro_patterns_to : Id.t move_location -> intro_pattern_expr located list ->
+val intro_patterns : intro_patterns -> unit Proofview.tactic
+val intro_patterns_to : Id.t move_location -> intro_patterns ->
   unit Proofview.tactic
-val intro_patterns_bound_to : int -> Id.t move_location ->
-  intro_pattern_expr located list -> unit Proofview.tactic
-val intro_pattern_to : Id.t move_location -> intro_pattern_expr ->
+val intro_patterns_bound_to : int -> Id.t move_location -> intro_patterns ->
+  unit Proofview.tactic
+val intro_pattern_to : Id.t move_location -> constr intro_pattern_expr ->
   unit Proofview.tactic
 
 (** Implements user-level "intros", with [] standing for "**" *)
-val intros_patterns : intro_pattern_expr located list -> unit Proofview.tactic
+val intros_patterns : intro_patterns -> unit Proofview.tactic
 
 (** {6 Exact tactics. } *)
 
@@ -193,7 +193,7 @@ val cut_and_apply         : constr -> unit Proofview.tactic
 val apply_in :
   advanced_flag -> evars_flag -> clear_flag -> Id.t -> 
     (clear_flag * constr with_bindings located) list ->
-    intro_pattern_expr located option -> unit Proofview.tactic
+    intro_pattern option -> unit Proofview.tactic
 
 (** {6 Elimination tactics. } *)
 
@@ -270,7 +270,7 @@ val induction : evars_flag ->
   (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
     intro_pattern_naming_expr located option *
-    or_and_intro_pattern_expr located option ->
+    constr or_and_intro_pattern_expr located option ->
       clause option -> unit Proofview.tactic
 
 (** {6 Case analysis tactics. } *)
@@ -283,7 +283,7 @@ val destruct : evars_flag ->
   (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
     intro_pattern_naming_expr located option *
-    or_and_intro_pattern_expr located option ->
+    constr or_and_intro_pattern_expr located option ->
       clause option -> unit Proofview.tactic
 
 (** {6 Generic case analysis / induction tactics. } *)
@@ -293,7 +293,7 @@ val destruct : evars_flag ->
 val induction_destruct : rec_flag -> evars_flag ->
   ((evar_map * constr with_bindings) induction_arg *
   (intro_pattern_naming_expr located option *
-   or_and_intro_pattern_expr located option))
+   constr or_and_intro_pattern_expr located option))
   list *
   constr with_bindings option *
   clause option -> unit Proofview.tactic
@@ -349,7 +349,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic
 val assert_after  : Name.t -> types -> unit Proofview.tactic
 
 val assert_as     : (* true = before *) bool ->
-  intro_pattern_expr located option -> constr -> unit Proofview.tactic
+  intro_pattern option -> constr -> unit Proofview.tactic
 
 (** Implements the tactics assert, enough and pose proof; note that "by"
     applies on the first goal for both assert and enough *)
@@ -364,7 +364,7 @@ val pose_proof : Name.t -> constr ->
 (** Common entry point for user-level "assert", "enough" and "pose proof" *)
 
 val forward   : bool -> unit Proofview.tactic option ->
-  intro_pattern_expr located option -> constr -> unit Proofview.tactic
+  intro_pattern option -> constr -> unit Proofview.tactic
 
 (** Implements the tactic cut, actually a modus ponens rule *)