From 04dfb014ae67e1446aba386913131e18e6bbe41f Mon Sep 17 00:00:00 2001
From: coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 19 Aug 2002 18:21:04 +0000
Subject: 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
---
 kernel/entries.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 4d86d6d2c..edba6e608 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -78,10 +78,13 @@ and module_type_entry =
     MTEident of kernel_name
   | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
   | MTEsig of mod_self_id * module_signature_entry
+  | MTEwith of module_type_entry * with_declaration
 
 and module_signature_entry = (label * specification_entry) list
 
-
+and with_declaration = 
+    With_Module of identifier * module_path
+  | With_Definition of identifier * constr
 
 and module_expr = 
     MEident of module_path
-- 
cgit v1.2.3