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 | |
| 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
| -rw-r--r-- | doc/syntax-v8.tex | 2 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 1 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 17 |
3 files changed, 11 insertions, 9 deletions
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex index 3276b72121..53e191e98f 100644 --- a/doc/syntax-v8.tex +++ b/doc/syntax-v8.tex @@ -981,7 +981,7 @@ $$ \nlsep \TERM{Add}~\OPT{\TERM{Rec}}~\TERM{ML}~\TERM{Path}~\NT{string} %% \nlsep \KWD{Type}~\NT{constr} -\nlsep \TERM{Print}~\OPT{\NT{printable}} +\nlsep \TERM{Print}~\NT{printable} \nlsep \TERM{Print}~\NT{reference} \nlsep \TERM{Inspect}~\NT{num} \nlsep \TERM{About}~\NT{reference} diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index d62d40d33b..79500c2366 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -483,7 +483,6 @@ GEXTEND Gram (* Printing (careful factorization of entries) *) | IDENT "Print"; p = printable -> VernacPrint p | IDENT "Print"; qid = global -> VernacPrint (PrintName qid) - | IDENT "Print" -> VernacPrint PrintLocalContext | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> VernacPrint (PrintModuleType qid) | IDENT "Print"; IDENT "Module"; qid = global -> 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 () |