From 8a7aff349c0a451eafead79abd4167f60249a7fb Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 12 Sep 2014 09:29:06 +0200
Subject: 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.---
 printing/pptactic.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b6b8c9c2e7..647d5702e0 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) =
 
-- 
cgit v1.2.3