diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-18 15:34:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-18 15:34:12 +0000 |
| commit | 600c1239019bb042f32764a93f46df17938d51c1 (patch) | |
| tree | c773a9c242ec07449338f74459755107c51be61b /parsing/g_vernac.ml4 | |
| parent | 7d1a2a61b9ba3d2d36ec51652d9f86280645fb83 (diff) | |
Plusieurs arguments autorisés pour Require et Read Module
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index caae9a1e4..0c2a61896 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -429,10 +429,11 @@ GEXTEND Gram <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec) ($STR $mname) ($STR $fname))>> *) - | IDENT "Read"; IDENT "Module"; qid = qualidarg -> - <:ast< (ReadModule $qid) >> + | IDENT "Read"; IDENT "Module"; qidl = LIST1 qualidarg -> + <:ast< (ReadModule ($LIST $qidl)) >> | IDENT "Require"; import = import_tok; specif = specif_tok; - qid = qualidarg -> <:ast< (Require $import $specif $qid) >> + qidl = LIST1 qualidarg -> + <:ast< (Require $import $specif ($LIST $qidl)) >> | IDENT "Require"; import = import_tok; specif = specif_tok; qid = qualidarg; filename = stringarg -> <:ast< (RequireFrom $import $specif $qid $filename) >> @@ -442,8 +443,10 @@ GEXTEND Gram <:ast< (WriteModule $id $s) >> | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = ne_stringarg_list -> <:ast< (DeclareMLModule ($LIST $l)) >> - | IDENT "Import"; qid = qualidarg -> <:ast< (ImportModule $qid) >> - + | IDENT "Import"; qidl = ne_qualidarg_list -> + <:ast< (ImportModule ($LIST $qidl)) >> + | IDENT "Export"; qidl = ne_qualidarg_list -> + <:ast< (ExportModule ($LIST $qidl)) >> ] ] ; |