diff options
| author | herbelin | 2004-01-29 13:31:40 +0000 |
|---|---|---|
| committer | herbelin | 2004-01-29 13:31:40 +0000 |
| commit | 5d623b0b32d987387aa9f47c87bc6779b7a9216e (patch) | |
| tree | 711d453516231a2497edd909b1b79e33ef7f1952 /translate | |
| parent | 0d579625ec962e199b6b9bc153817080611e8016 (diff) | |
Suppression de 'Print.' en v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5265 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index c60e5d87ca..7689014982 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -948,12 +948,11 @@ let rec pr_vernac = function prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr pr_pattern - | VernacSyntacticDefinition (id,c,None) -> - hov 2 (str"Syntactic Definition " ++ pr_lident id ++ str" :=" ++ - pr_lconstrarg c) - | VernacSyntacticDefinition (id,c,Some n) -> - hov 2 (str"Syntactic Definition " ++ pr_lident id ++ str" :=" ++ - pr_lconstrarg c ++ spc() ++ str"|" ++ int n) + | VernacSyntacticDefinition (id,c,local,onlyparsing) -> + hov 2 + (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++ + pr_constrarg c ++ + pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) | VernacDeclareImplicits (q,None) -> hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) | VernacDeclareImplicits (q,Some l) -> @@ -1031,7 +1030,8 @@ let rec pr_vernac = function | PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s | PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt | PrintName qid -> str"Print" ++ spc() ++ pr_reference qid - | PrintLocalContext -> str"Print" + | PrintLocalContext -> assert false + (* str"Print" *) | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid | PrintInspect n -> str"Inspect" ++ spc() ++ int n @@ -1116,5 +1116,8 @@ let pr_vernac = function let a = Names.string_of_id a in a = "nat_scope" or a = "Z_scope" or a = "R_scope" -> mt() | VernacSyntax _ | VernacGrammar _ as x -> pr_vernac x + | VernacPrint PrintLocalContext -> + warning ("\"Print.\" is discontinued"); + mt () | x -> pr_vernac x ++ sep_end () |