diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1d7a9428..4103ea00 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml,v 1.54.2.3 2005/01/15 14:56:53 herbelin Exp $ *) +(* $Id: pptactic.ml,v 1.54.2.5 2005/12/23 22:16:46 herbelin Exp $ *) open Pp open Names @@ -42,6 +42,8 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) = Hashtbl.add prtac_tab_v7 (s,tags) prods; if for_v8 then Hashtbl.add prtac_tab (s,tags) prods +let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags) + type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -536,7 +538,8 @@ and pr_atom1 = function | TacTrivial (Some []) as x -> pr_atom0 x | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db) | TacAuto (None,Some []) as x -> pr_atom0 x - | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db) + | TacAuto (n,db) -> + hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db) | TacAutoTDB None as x -> pr_atom0 x | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n) | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id) @@ -546,7 +549,8 @@ and pr_atom1 = function hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2) | TacDAuto (n,p) -> - hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p) + hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++ + pr_opt int p) (* Context management *) | TacClear l -> |