diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3305acb7..6e13d4e9 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -515,6 +515,11 @@ let pr_auto_using prc = function | l -> spc () ++ hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l) +let string_of_debug = function + | Off -> "" + | Debug -> "debug " + | Info -> "info_" + let pr_then () = str ";" let ltop = (5,E) @@ -623,19 +628,14 @@ let rec pr_atom0 = function | TacAssumption -> str "assumption" | TacAnyConstructor (false,None) -> str "constructor" | TacAnyConstructor (true,None) -> str "econstructor" - | TacTrivial ([],Some []) -> str "trivial" - | TacAuto (None,[],Some []) -> str "auto" + | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial") + | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto") | TacReflexivity -> str "reflexivity" | TacClear (true,[]) -> str "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" (* Main tactic printer *) and pr_atom1 = function - | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl - | TacSuperAuto _ | TacExtend (_, - ("GTauto"|"GIntuition"|"TSimplif"| - "LinearIntuition"),_) -> - errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0") | TacExtend (loc,s,l) -> pr_with_comments loc (pr_extend 1 s l) | TacAlias (loc,s,l,_) -> @@ -742,17 +742,15 @@ and pr_atom1 = function hov 1 (str "lapply" ++ pr_constrarg c) (* Automation tactics *) - | TacTrivial ([],Some []) as x -> pr_atom0 x - | TacTrivial (lems,db) -> - hov 0 (str "trivial" ++ + | TacTrivial (_,[],Some []) as x -> pr_atom0 x + | TacTrivial (d,lems,db) -> + hov 0 (str (string_of_debug d ^ "trivial") ++ pr_auto_using pr_constr lems ++ pr_hintbases db) - | TacAuto (None,[],Some []) as x -> pr_atom0 x - | TacAuto (n,lems,db) -> - hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ + | TacAuto (_,None,[],Some []) as x -> pr_atom0 x + | TacAuto (d,n,lems,db) -> + hov 0 (str (string_of_debug d ^ "auto") ++ + pr_opt (pr_or_var int) n ++ pr_auto_using pr_constr lems ++ pr_hintbases db) - | TacDAuto (n,p,lems) -> - hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ - pr_opt int p ++ pr_auto_using pr_constr lems) (* Context management *) | TacClear (true,[]) as t -> pr_atom0 t |