Replace the list of argument in tacexpr with a single row argument.

This has several benefits
* It replicates the "no quadrillion-uple" pattern at the level of types. Giving names to the various component will hopefully make for better error messages.
* It is less typo-prone, as the whole row can be passed as an argument rather than retyping each of the arguments. Also makes for a terser [Tacexpr].
* More importantly: local changes to tactic expressions will more often be kept local. Which will avoid some extra tedious work, and make rebases on top of such changes significantly easier.

2 files changed, 118 insertions, 55 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 55d6e53a5..3501917f2 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -119,7 +119,7 @@ type intro_pattern_naming = intro_pattern_naming_expr located
 
 (** Generic expressions for atomic tactics *)
 
-type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr =
+type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of 'trm intro_pattern_expr located list
   | TacIntroMove of Id.t option * 'nam move_location
@@ -133,7 +133,7 @@ type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
-      bool * ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr option *
+      bool * 'a gen_tactic_expr option *
       'trm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacGeneralizeDep of 'trm
@@ -168,12 +168,21 @@ type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr =
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
       (bool * multi * 'trm with_bindings_arg) list * 'nam clause_expr *
-      ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr option
+      'a gen_tactic_expr option
   | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
 
+constraint 'a = <
+    term:'trm;
+    pattern:'pat;
+    constant:'cst;
+    reference:'ref;
+    name:'nam;
+    level:'lev
+>
+
 (** Possible arguments of a tactic definition *)
 
-and ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg =
+and 'a gen_tactic_arg =
   | TacDynamic     of Loc.t * Dyn.t
   | TacGeneric     of 'lev generic_argument
   | MetaIdArg      of Loc.t * bool * string
@@ -184,77 +193,104 @@ and ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg =
                                is not a variant of [tactic_expr]. *)
   | Reference      of 'ref
   | TacCall of Loc.t * 'ref *
-      ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list
+      'a gen_tactic_arg list
   | TacFreshId of string or_var list
-  | Tacexp of ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr
+  | Tacexp of 'a gen_tactic_expr
   | TacPretype of 'trm
   | TacNumgoals
 
+constraint 'a = <
+    term:'trm;
+    pattern:'pat;
+    constant:'cst;
+    reference:'ref;
+    name:'nam;
+    level:'lev
+>
+
 (** Generic ltac expressions.
     't : terms, 'p : patterns, 'c : constants, 'i : inductive,
     'r : ltac refs, 'n : idents, 'l : levels *)
 
-and ('t,'p,'c,'r,'n,'l) gen_tactic_expr =
-  | TacAtom of Loc.t * ('t,'p,'c,'r,'n,'l) gen_atomic_tactic_expr
+and 'a gen_tactic_expr =
+  | TacAtom of Loc.t * 'a gen_atomic_tactic_expr
   | TacThen of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
   | TacDispatch of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr list
+      'a gen_tactic_expr list
   | TacExtendTac of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr array *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr array
+      'a gen_tactic_expr array *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array
   | TacThens of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr list
+      'a gen_tactic_expr *
+      'a gen_tactic_expr list
   | TacThens3parts of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr array *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr array
-  | TacFirst of ('t,'p,'c,'r,'n,'l) gen_tactic_expr list
-  | TacComplete of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
-  | TacSolve of ('t,'p,'c,'r,'n,'l) gen_tactic_expr list
-  | TacTry of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr array
+  | TacFirst of 'a gen_tactic_expr list
+  | TacComplete of 'a gen_tactic_expr
+  | TacSolve of 'a gen_tactic_expr list
+  | TacTry of 'a gen_tactic_expr
   | TacOr of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
   | TacOnce of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+      'a gen_tactic_expr
   | TacExactlyOnce of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+      'a gen_tactic_expr
   | TacOrelse of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr
-  | TacDo of int or_var * ('t,'p,'c,'r,'n,'l) gen_tactic_expr
-  | TacTimeout of int or_var * ('t,'p,'c,'r,'n,'l) gen_tactic_expr
-  | TacTime of string option * ('t,'p,'c,'r,'n,'l) gen_tactic_expr
-  | TacRepeat of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
-  | TacProgress of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
-  | TacShowHyps of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
+  | TacDo of int or_var * 'a gen_tactic_expr
+  | TacTimeout of int or_var * 'a gen_tactic_expr
+  | TacTime of string option * 'a gen_tactic_expr
+  | TacRepeat of 'a gen_tactic_expr
+  | TacProgress of 'a gen_tactic_expr
+  | TacShowHyps of 'a gen_tactic_expr
   | TacAbstract of
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr * Id.t option
+      'a gen_tactic_expr * Id.t option
   | TacId of 'n message_token list
   | TacFail of int or_var * 'n message_token list
-  | TacInfo of ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+  | TacInfo of 'a gen_tactic_expr
   | TacLetIn of rec_flag *
-      (Id.t located * ('t,'p,'c,'r,'n,'l) gen_tactic_arg) list *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+      (Id.t located * 'a gen_tactic_arg) list *
+      'a gen_tactic_expr
   | TacMatch of lazy_flag *
-      ('t,'p,'c,'r,'n,'l) gen_tactic_expr *
-      ('p,('t,'p,'c,'r,'n,'l) gen_tactic_expr) match_rule list
+      'a gen_tactic_expr *
+      ('p,'a gen_tactic_expr) match_rule list
   | TacMatchGoal of lazy_flag * direction_flag *
-      ('p,('t,'p,'c,'r,'n,'l) gen_tactic_expr) match_rule list
-  | TacFun of ('t,'p,'c,'r,'n,'l) gen_tactic_fun_ast
-  | TacArg of ('t,'p,'c,'r,'n,'l) gen_tactic_arg located
+      ('p,'a gen_tactic_expr) match_rule list
+  | TacFun of 'a gen_tactic_fun_ast
+  | TacArg of 'a gen_tactic_arg located
   (* For ML extensions *)
   | TacML of Loc.t * ml_tactic_name * 'l generic_argument list
   (* For syntax extensions *)
   | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list
 
-and ('t,'p,'c,'r,'n,'l) gen_tactic_fun_ast =
-    Id.t option list * ('t,'p,'c,'r,'n,'l) gen_tactic_expr
+constraint 'a = <
+    term:'t;
+    pattern:'p;
+    constant:'c;
+    reference:'r;
+    name:'n;
+    level:'l
+>
+
+and 'a gen_tactic_fun_ast =
+    Id.t option list * 'a gen_tactic_expr
+
+constraint 'a = <
+    term:'t;
+    pattern:'p;
+    constant:'c;
+    reference:'r;
+    name:'n;
+    level:'l
+>
 
 (** Globalized tactics *)
 
@@ -264,14 +300,23 @@ type g_cst = evaluable_global_reference and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam  = Id.t located
 
+type g_dispatch =  <
+    term:g_trm;
+    pattern:g_pat;
+    constant:g_cst;
+    reference:g_ref;
+    name:g_nam;
+    level:glevel
+>
+
 type glob_tactic_expr =
-    (g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_tactic_expr
+    g_dispatch gen_tactic_expr
 
 type glob_atomic_tactic_expr =
-    (g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_atomic_tactic_expr
+    g_dispatch gen_atomic_tactic_expr
 
 type glob_tactic_arg =
-    (g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_tactic_arg
+    g_dispatch gen_tactic_arg
 
 (** Raw tactics *)
 
@@ -282,14 +327,23 @@ type r_ref = reference
 type r_nam  = Id.t located
 type r_lev = rlevel
 
+type r_dispatch =  <
+    term:r_trm;
+    pattern:r_pat;
+    constant:r_cst;
+    reference:r_ref;
+    name:r_nam;
+    level:rlevel
+>
+
 type raw_atomic_tactic_expr =
-    (r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_atomic_tactic_expr
+    r_dispatch gen_atomic_tactic_expr
 
 type raw_tactic_expr =
-    (r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_tactic_expr
+    r_dispatch gen_tactic_expr
 
 type raw_tactic_arg =
-    (r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_tactic_arg
+    r_dispatch gen_tactic_arg
 
 (** Misc *)
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b6b8c9c2e..647d5702e 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -608,8 +608,8 @@ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
 (** A printer for tactics that polymorphically works on the three
     "raw", "glob" and "typed" levels *)
 
-type ('trm,'pat,'cst,'ref,'nam,'lev) printer = {
-  pr_tactic : tolerability -> ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr -> std_ppcmds;
+type 'a printer = {
+  pr_tactic : tolerability -> 'a gen_tactic_expr -> std_ppcmds;
   pr_constr : 'trm -> std_ppcmds;
   pr_lconstr : 'trm -> std_ppcmds;
   pr_pattern : 'pat -> std_ppcmds;
@@ -622,6 +622,15 @@ type ('trm,'pat,'cst,'ref,'nam,'lev) printer = {
   pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
 }
 
+constraint 'a = <
+    term:'trm;
+    pattern:'pat;
+    constant:'cst;
+    reference:'ref;
+    name:'nam;
+    level:'lev
+>
+
 let make_pr_tac pr
   (strip_prod_binders) =