diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 01:31:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 01:57:19 +0100 |
| commit | 0af598b77a6242d796c66884477a046448ef1e21 (patch) | |
| tree | f0baff4fff51d0f6b785dafd01051aa37eb1c240 /printing/ppvernac.ml | |
| parent | 8cb2040e4af40594826df97a735c38c8882934ca (diff) | |
Moving Tactic Notation to an EXTEND based command.
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 887a14d2b..88bb805a7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -378,17 +378,6 @@ module Make | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - let print_level n = - if not (Int.equal n 0) then - spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")") - else - mt () - - let pr_grammar_tactic_rule n (_,pil,t) = - hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++ - hov 0 (prlist_with_sep sep pr_production_item pil ++ - spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) - let pr_univs pl = match pl with | None -> mt () @@ -644,8 +633,6 @@ module Make return (keyword "No-parsing-rule for VernacError") (* Syntax *) - | VernacTacticNotation (n,r,e) -> - return (pr_grammar_tactic_rule n ("",r,e)) | VernacOpenCloseScope (_,(opening,sc)) -> return ( keyword (if opening then "Open " else "Close ") ++ |