diff options
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 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 |