From 9c18de511b7d54fdecc44cadb56c760da3498a39 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 26 Nov 2003 19:03:23 +0000
Subject: Traduction de tactic:constrarg en constr:constr pour les arguments de
 Tactic Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4996 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernacnew.ml4  | 1 +
 translate/ppvernacnew.ml | 1 +
 2 files changed, 2 insertions(+)

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 4ea3368532..616cdfd75d 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -746,6 +746,7 @@ GEXTEND Gram
   non_terminal:
     [[ u = IDENT; ":"; nt = IDENT ->
         NtQual(rename_command_entry u, rename_command_entry nt)
+     | IDENT "constr" -> NtQual ("constr","constr")
      | nt = IDENT -> NtShort (rename_command_entry nt) ]]
   ;
 END
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index fd16ef5ade..87f4a7b5f5 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -127,6 +127,7 @@ let pr_set_entry_type = function
 
 let pr_non_terminal = function
   | NtQual (u,nt) -> str u ++ str" : " ++ str nt
+  | NtShort "constrarg" -> str "constr"
   | NtShort nt -> str nt
 
 let strip_meta id =
-- 
cgit v1.2.3