diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 00:02:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 01:15:43 +0200 |
| commit | 243ffa4b928486122075762da6ce8da707e07daf (patch) | |
| tree | 3870e1b1d3059ba13158a73df7c5f3b300e504ce /printing | |
| parent | 6dd9e003c289a79b0656e7c6f2cc59935997370c (diff) | |
Moving the TacExtend node from atomic to plain tactics.
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 02a21ced6..c183cb160 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -654,8 +654,6 @@ let rec pr_atom0 = function (* Main tactic printer *) and pr_atom1 = function - | TacExtend (loc,s,l) -> - pr_with_comments loc (pr_extend 1 s l) | TacAlias (loc,kn,l) -> pr_with_comments loc (pr_alias 1 kn (List.map snd l)) @@ -938,6 +936,8 @@ let rec pr_tac inherited tac = prlist_with_sep spc pr_tacarg l)), lcall | TacArg (_,a) -> pr_tacarg a, latom + | TacML (loc,s,l) -> + pr_with_comments loc (pr_extend 1 s l), lcall in if prec_less prec inherited then strm else str"(" ++ strm ++ str")" |