diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 14:47:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 14:47:16 +0000 |
| commit | ef41c3d1f93e2fa82cbaa97adaa03852e8fcd7b8 (patch) | |
| tree | 83e1275bde041c78bc7411e80a49e56cad4ac446 /parsing | |
| parent | d3407458889d4ba4ff6fbf465a92c86976c01ba5 (diff) | |
'Implicits qid' -> 'Implicit Arguments qid'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4320 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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) |