From 04dfb014ae67e1446aba386913131e18e6bbe41f Mon Sep 17 00:00:00 2001
From: coq
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/declarations.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8b11705970..05989bc82a 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -148,7 +148,8 @@ and module_expr_body =
   | MEBapply of module_expr_body * module_expr_body
       * constraints
 
-and module_specification_body = module_type_body * module_path option
+and module_specification_body = 
+    module_type_body * module_path option * constraints
 
 and structure_elem_body = 
   | SEBconst of constant_body
@@ -160,6 +161,7 @@ and module_structure_body = (label * structure_elem_body) list
 
 and module_body = 
     { mod_expr : module_expr_body option;
-      mod_user_type : (module_type_body * constraints) option;
+      mod_user_type : module_type_body option;
       mod_type : module_type_body;
-      mod_equiv : module_path option }
+      mod_equiv : module_path option;
+      mod_constraints : constraints }
-- 
cgit v1.2.3