diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-19 18:21:04 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-19 18:21:04 +0000 |
| commit | 04dfb014ae67e1446aba386913131e18e6bbe41f (patch) | |
| tree | f36c281209313783b176473117f910f3818dd658 /parsing/g_module.ml4 | |
| parent | f0591d4fdf4a39c53ee690fc7285b592161406de (diff) | |
La notation 'with'. L'interpretation - version preliminaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_module.ml4')
| -rw-r--r-- | parsing/g_module.ml4 | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4 index 01e7256ef..56db0cb59 100644 --- a/parsing/g_module.ml4 +++ b/parsing/g_module.ml4 @@ -73,9 +73,18 @@ GEXTEND Gram ] ] ; + with_declaration: + [ [ "Definition"; id = ident; ":="; c = Constr.constr -> + <:ast< (WITHDEFINITION $id $c) >> + | IDENT "Module"; id = ident; ":="; qid = qualid -> + <:ast< (WITHMODULE $id $qid) >> + ] ] + ; + module_type: [ [ qid = qualid -> <:ast< (MODTYPEQID $qid) >> (* ... *) - ] ] + | mty = module_type; "with"; decl = with_declaration -> + <:ast< (MODTYPEWITH $mty $decl)>> ] ] ; END |