diff options
| author | letouzey | 2012-10-06 10:08:24 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-06 10:08:24 +0000 |
| commit | 8e10368c387570df13904531bfba05130335ed0e (patch) | |
| tree | 50d7a35c9a45e0c9496da4a4ad22ead531be829d /printing | |
| parent | 2e3cf396ba869987c4e41f46bc9b4b2fe31ab4d2 (diff) | |
Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box
Nested was never constructed, while the notion of abstract_tactic_box
is obsolete (cf. Refiner.abstract_tactic).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/tactic_printer.ml | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml index 87bb89e8d4..49d7c21f6c 100644 --- a/printing/tactic_printer.ml +++ b/printing/tactic_printer.ml @@ -23,31 +23,16 @@ let pr_tactic = function let pr_rule = function | Prim r -> hov 0 (pr_prim_rule r) - | Nested(cmpd,_) -> - begin - match cmpd with - | Tactic (texp,_) -> hov 0 (pr_tactic texp) - end | Daimon -> str "<Daimon>" | Decl_proof _ -> str "proof" -let uses_default_tac = function - | Nested(Tactic(_,dflt),_) -> dflt - | _ -> false - (* Does not print change of evars *) let pr_rule_dot = function | Prim Change_evars ->str "PC: ch_evars" ++ mt () (* PC: this might be redundant *) - | r -> - pr_rule r ++ if uses_default_tac r then str "..." else str"." + | r -> pr_rule r ++ str"." let pr_rule_dot_fnl = function - | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_) - | TacMutualCofix (true,_,_))),_),_) -> - (* Very big hack to not display hidden tactics in "Theorem with" *) - (* (would not scale!) *) - mt () | Prim Change_evars -> mt () | r -> pr_rule_dot r ++ fnl () |