diff options
Diffstat (limited to 'parsing/g_module.ml4')
| -rw-r--r-- | parsing/g_module.ml4 | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4 deleted file mode 100644 index 0b542608..00000000 --- a/parsing/g_module.ml4 +++ /dev/null @@ -1,47 +0,0 @@ -(************************************************************************) -(* 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 |