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

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

2 files changed, 18 insertions, 12 deletions

diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 3d9a344ee..390711fab 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -16,20 +16,22 @@ type patvar = Id.t
 
 (** Introduction patterns *)
 
-type intro_pattern_expr =
+type 'constr intro_pattern_expr =
   | IntroForthcoming of bool
   | IntroNaming of intro_pattern_naming_expr
-  | IntroAction of intro_pattern_action_expr
+  | IntroAction of 'constr intro_pattern_action_expr
 and intro_pattern_naming_expr =
   | IntroWildcard
   | IntroIdentifier of Id.t
   | IntroFresh of Id.t
   | IntroAnonymous
-and intro_pattern_action_expr =
-  | IntroOrAndPattern of or_and_intro_pattern_expr
-  | IntroInjection of (Loc.t * intro_pattern_expr) list
+and 'constr intro_pattern_action_expr =
+  | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
+  | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list
+  | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr)
   | IntroRewrite of bool
-and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list
+and 'constr or_and_intro_pattern_expr =
+  (Loc.t * 'constr intro_pattern_expr) list list
 
 (** Move destination for hypothesis *)
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 2af77eb10..9b75282ca 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -44,9 +44,9 @@ type inversion_kind =
 
 type ('c,'id) inversion_strength =
   | NonDepInversion of
-      inversion_kind * 'id list * or_and_intro_pattern_expr located option
+      inversion_kind * 'id list * 'c or_and_intro_pattern_expr located option
   | DepInversion of
-      inversion_kind * 'c option * or_and_intro_pattern_expr located option
+      inversion_kind * 'c option * 'c or_and_intro_pattern_expr located option
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -59,7 +59,7 @@ type 'id message_token =
 type 'constr induction_clause =
     'constr with_bindings induction_arg *
     (intro_pattern_naming_expr located option (* eqn:... *)
-    * or_and_intro_pattern_expr located option) (* as ... *)
+    * 'constr or_and_intro_pattern_expr located option) (* as ... *)
 
 type ('constr,'id) induction_clause_list =
     'constr induction_clause list
@@ -106,15 +106,19 @@ type open_glob_constr = unit * glob_constr_and_expr
 
 type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
+type intro_pattern = Term.constr intro_pattern_expr located
+type intro_patterns = Term.constr intro_pattern_expr located list
+type or_and_intro_pattern = Term.constr or_and_intro_pattern_expr located
+
 (** Generic expressions for atomic tactics *)
 
 type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   (* Basic tactics *)
-  | TacIntroPattern of intro_pattern_expr located list
+  | TacIntroPattern of 'trm intro_pattern_expr located list
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      (clear_flag * 'nam * intro_pattern_expr located option) option
+      (clear_flag * 'nam * 'trm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacFix of Id.t option * int
@@ -123,7 +127,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
       bool * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
-      intro_pattern_expr located option * 'trm
+      'trm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacGeneralizeDep of 'trm
   | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *