diff options
| author | herbelin | 2003-03-12 13:23:18 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-12 13:23:18 +0000 |
| commit | df29f2f0257e0a69fa1eaa3c3ddcd56a80d14e0d (patch) | |
| tree | 30716fc849cc1c3426c5f503de4fc730bd04efe5 | |
| parent | 62d08f32993d7b3cfb1ce484ac6ac223dbedc6d9 (diff) | |
Ajout Locate Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3757 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | translate/ppvernacnew.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 2996c0aecc..bfebda362a 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -482,6 +482,7 @@ let rec pr_vernac = function | LocateTerm qid -> pr_reference qid | LocateFile f -> str"File" ++ spc() ++ qs f | LocateLibrary qid -> str"Library" ++ spc () ++ pr_reference qid + | LocateNotation s -> str ("\""^s^"\"") in str"Locate" ++ spc() ++ pr_locate loc | VernacComments l -> hov 1 (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) | VernacNop -> str"Proof" |