Reorganisation of intropattern code

- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns

Still some questions:

- Should -> and <- apply to hypotheses or not (currently they apply to
  hypotheses either when used in assert-style tactics or apply in, or
  when the term to rewrite is a variable, in which case "subst" is
  applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
  posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
  quantifications?

2 files changed, 13 insertions, 9 deletions

diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 6ee44215c0..3d9a344ee9 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -17,14 +17,18 @@ type patvar = Id.t
 (** Introduction patterns *)
 
 type intro_pattern_expr =
-  | IntroOrAndPattern of or_and_intro_pattern_expr
-  | IntroInjection of (Loc.t * intro_pattern_expr) list
+  | IntroForthcoming of bool
+  | IntroNaming of intro_pattern_naming_expr
+  | IntroAction of intro_pattern_action_expr
+and intro_pattern_naming_expr =
   | IntroWildcard
-  | IntroRewrite of bool
   | IntroIdentifier of Id.t
   | IntroFresh of Id.t
-  | IntroForthcoming of bool
   | IntroAnonymous
+and intro_pattern_action_expr =
+  | IntroOrAndPattern of or_and_intro_pattern_expr
+  | IntroInjection of (Loc.t * intro_pattern_expr) list
+  | IntroRewrite of bool
 and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list
 
 (** Move destination for hypothesis *)
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index cf8d34d7e7..2af77eb103 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 * intro_pattern_expr located option
+      inversion_kind * 'id list * or_and_intro_pattern_expr located option
   | DepInversion of
-      inversion_kind * 'c option * intro_pattern_expr located option
+      inversion_kind * 'c option * or_and_intro_pattern_expr located option
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -58,8 +58,8 @@ type 'id message_token =
 
 type 'constr induction_clause =
     'constr with_bindings induction_arg *
-    (intro_pattern_expr located option (* eqn:... *)
-    * intro_pattern_expr located option) (* as ... *)
+    (intro_pattern_naming_expr located option (* eqn:... *)
+    * or_and_intro_pattern_expr located option) (* as ... *)
 
 type ('constr,'id) induction_clause_list =
     'constr induction_clause list
@@ -127,7 +127,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacGeneralizeDep of 'trm
   | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
-      intro_pattern_expr located option
+      intro_pattern_naming_expr located option
 
   (* Derived basic tactics *)
   | TacInductionDestruct of