From df29f2f0257e0a69fa1eaa3c3ddcd56a80d14e0d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 12 Mar 2003 13:23:18 +0000
Subject: Ajout Locate Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3757 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/ppvernacnew.ml | 1 +
 1 file changed, 1 insertion(+)

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"
-- 
cgit v1.2.3