diff options
| author | herbelin | 2004-01-20 08:44:31 +0000 |
|---|---|---|
| committer | herbelin | 2004-01-20 08:44:31 +0000 |
| commit | 39efc2b2fffab68aae5b1e0be9920fdbf4f1859d (patch) | |
| tree | 70125691b07d3b286b4f8807fd1b129c138ef9bf | |
| parent | 36db515b0e02756602551c6dc82b6b6783e56ae5 (diff) | |
Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5220 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 8808ef0258..e866d01723 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -428,17 +428,7 @@ GEXTEND Gram VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; - idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) - - (* For compatibility *) - | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" -> - VernacSetOption - (Goptions.SecondaryTable ("Implicit","Arguments"), - BoolValue true) - | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off" -> - VernacSetOption - (Goptions.SecondaryTable ("Implicit","Arguments"), - BoolValue false) ] ] + idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ] ; END |