diff options
| author | mohring | 2002-12-04 17:09:57 +0000 |
|---|---|---|
| committer | mohring | 2002-12-04 17:09:57 +0000 |
| commit | 885673cbec549d24bd57b9e16bfb5375e426101c (patch) | |
| tree | c3693a4e70758d70e9706f7f98c54f6f1bfa0ab7 /parsing | |
| parent | cc92b9228f3463ce06ad457a47ef2a9b1f39a727 (diff) | |
Modification Require From
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3376 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e94b513fb4..30c0d368be 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -467,9 +467,12 @@ GEXTEND Gram VernacRequire (None, None, qidl) | IDENT "Require"; export = export_token; specif = specif_token; qidl = LIST1 global -> VernacRequire (Some export, specif, qidl) - | IDENT "Require"; export = export_token; specif = specif_token; +(* | IDENT "Require"; export = export_token; specif = specif_token; id = base_ident; filename = STRING -> - VernacRequireFrom (export, specif, id, filename) + VernacRequireFrom (export, specif, id, filename) *) + | IDENT "Require"; export = export_token; specif = specif_token; + filename = STRING -> + VernacRequireFrom (export, specif, filename) | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING -> VernacDeclareMLModule l | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) |