diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-13 17:16:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-13 17:16:30 +0000 |
| commit | 4c18a78b54ff33361990a6f19bcad69bb7a4417c (patch) | |
| tree | 68439997aff6fe7981a81032380183479f11e050 /translate | |
| parent | ad378c77378dd492d073ed4732390da7df58ce3e (diff) | |
Traduction Print Grammar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 42c518e5a..916204968 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -994,7 +994,8 @@ let rec pr_vernac = function | PrintSectionContext s -> str"Print Section" ++ spc() ++ Libnames.pr_reference s | PrintGrammar (uni,ent) -> - str"Print Grammar" ++ spc() ++ str uni ++ spc() ++ str ent + msgerrnl (str "warning: no direct translation of Print Grammar entry"); + str"Print Grammar" ++ spc() ++ str ent | PrintLoadPath -> str"Print LoadPath" | PrintModules -> str"Print Modules" | PrintMLLoadPath -> str"Print ML Path" |