diff options
| author | Arnaud Spiwack | 2014-09-12 09:29:06 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-12 10:17:22 +0200 |
| commit | 8a7aff349c0a451eafead79abd4167f60249a7fb (patch) | |
| tree | 2a87b649c3d61a2c3a5214610d69218febc1c89e /printing/pptactic.ml | |
| parent | ad86932abc23df9139065d453771a190df365928 (diff) | |
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.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 13 |
1 files changed, 11 insertions, 2 deletions
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) = |