diff options
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 31daf4afd..3c1fad5d1 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -443,8 +443,6 @@ GEXTEND Gram pos = OPT [ "["; l = LIST0 natural; "]" -> l ] -> VernacDeclareImplicits (qid,pos) - | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None) - | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"]; idl = LIST1 ident; ":"; c = constr -> VernacReserve (idl,c) |