Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5426 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 3 deletions

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 44599e72f5..cfeb12f06c 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -132,8 +132,7 @@ let pr_set_entry_type = function
   | ETBigint -> str "bigint"
 
 let pr_non_terminal = function
-  | NtQual ("constr","constr") -> str "constr"
-  | NtQual (u,nt) -> str u ++ str" : " ++ str nt
+  | NtQual (u,nt) -> (* no more qualified entries *) str nt
   | NtShort "constrarg" -> str "constr"
   | NtShort nt -> str nt
 
@@ -416,7 +415,7 @@ let pr_grammar_tactic_rule (name,(s,pil),t) =
 *)
   hov 2 (str "Tactic Notation" ++ spc() ++ 
     hov 0 (qsnew s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++
-    spc() ++ str":= " ++ spc() ++ pr_raw_tactic t))
+    spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
 
 let pr_box b = let pr_boxkind = function
   | PpHB n -> str"h" ++ spc() ++ int n