From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 parsing/g_module.ml4 | 47 -----------------------------------------------
 1 file changed, 47 deletions(-)
 delete mode 100644 parsing/g_module.ml4

(limited to 'parsing/g_module.ml4')

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
-- 
cgit v1.2.3