diff options
Diffstat (limited to 'parsing/g_module.ml4')
| -rw-r--r-- | parsing/g_module.ml4 | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4 new file mode 100644 index 00000000..0b542608 --- /dev/null +++ b/parsing/g_module.ml4 @@ -0,0 +1,47 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: g_module.ml4,v 1.6.2.1 2004/07/16 19:30:39 herbelin Exp $ *) + +open Pp +open Ast +open Pcoq +open Prim +open Module +open Util +open Topconstr + +(* Grammar rules for module expressions and types *) + +if !Options.v7 then +GEXTEND Gram + GLOBAL: module_expr module_type; + + module_expr: + [ [ qid = qualid -> CMEident qid + | me1 = module_expr; me2 = module_expr -> CMEapply (me1,me2) + | "("; me = module_expr; ")" -> me +(* ... *) + ] ] + ; + + with_declaration: + [ [ "Definition"; id = identref; ":="; c = Constr.constr -> + CWith_Definition (id,c) + | IDENT "Module"; id = identref; ":="; qid = qualid -> + CWith_Module (id,qid) + ] ] + ; + + module_type: + [ [ qid = qualid -> CMTEident qid +(* ... *) + | mty = module_type; "with"; decl = with_declaration -> + CMTEwith (mty,decl) ] ] + ; +END |