diff options
| author | herbelin | 2005-12-26 20:07:21 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-26 20:07:21 +0000 |
| commit | 52f4136ecf452162adb55c8de031b73c97dcdbac (patch) | |
| tree | 8ac0a4c3584025a44067c6a96c6ce9d92ca93e78 /parsing/g_module.ml4 | |
| parent | 099fb1b4c5084bb899e4910e42c971cdfa81e1aa (diff) | |
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
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 e1937b5f9b..0000000000 --- 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$ *) - -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"; fqid = fullyqualid; ":="; c = Constr.constr -> - CWith_Definition (fqid,c) - | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> - CWith_Module (fqid,qid) - ] ] - ; - - module_type: - [ [ qid = qualid -> CMTEident qid -(* ... *) - | mty = module_type; "with"; decl = with_declaration -> - CMTEwith (mty,decl) ] ] - ; -END |