diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-14 10:54:28 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-14 10:54:28 +0000 |
| commit | 7e787bce059ea8c69caadfc31110c648c3837b9c (patch) | |
| tree | b00d786d92b1a366040e5c33024599213a6c914b /parsing/g_vernac.ml4 | |
| parent | af0a1bfa3a277c15c4881bed3ceb99dda81c9362 (diff) | |
reparations suite a la nouvelle syntaxe:
- syntaxe des modules
- syntaxe existentielle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3769 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index dadef23dd..d60a4db73 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -327,14 +327,15 @@ GEXTEND Gram IDENT "Section"; id = base_ident -> VernacBeginSection id | IDENT "Chapter"; id = base_ident -> VernacBeginSection id ] ] ; - module_vardecls: - [ [ "("; id = base_ident; idl = ident_comma_list_tail; - ":"; mty = Module.module_type; ")" - -> (id::idl,mty) ] ] + [ [ id = base_ident; idl = ident_comma_list_tail; ":"; + mty = Module.module_type -> (id::idl,mty) ] ] + ; + module_binders: + [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ] ; module_binders_list: - [ [ bl = LIST0 module_vardecls -> bl ] ] + [ [ bls = LIST0 module_binders -> List.flatten bls ] ] ; of_module_type: [ [ ":"; mty = Module.module_type -> (mty, true) |