From 67787e6daeb7bf2fe59d5546969197ca9f87c2dc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Mar 2003 14:06:47 +0000
Subject: Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4    | 3 +++
 parsing/g_vernacnew.ml4 | 3 +++
 2 files changed, 6 insertions(+)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d60a4db73a..cb02b082e4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -424,6 +424,9 @@ GEXTEND Gram
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
 
+      | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
+	   idl = LIST1 ident SEP ","; ":"; c = constr -> VernacReserve (idl,c)
+
       (* For compatibility *)
       | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
 	  VernacSetOption
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 8830001119..12e95d235a 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -423,6 +423,9 @@ GEXTEND Gram
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
 
+      | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
+	   idl = LIST1 ident; ":"; c = constr -> VernacReserve (idl,c)
+
       (* For compatibility *)
       | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
 	  VernacSetOption
-- 
cgit v1.2.3