diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-29 14:06:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-29 14:06:47 +0000 |
| commit | 67787e6daeb7bf2fe59d5546969197ca9f87c2dc (patch) | |
| tree | cb5d2bb991afcfcb53d879aa37d2a2187c90ca9c /parsing | |
| parent | 5193d92186e14794a346392af4d80fc264d8fff7 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 3 |
2 files changed, 6 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d60a4db73..cb02b082e 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 883000111..12e95d235 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 |