From d1df4f36c4e304d6ed446d09b64d1b3bf34bac16 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 15 Oct 2008 15:07:10 +0000
Subject: Report des commits 11417 et 11437 de la v8.2

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11454 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e98cb379c2..fb8317cdcb 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -182,7 +182,8 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * constraints option
+  | SFBalias of module_path * struct_expr_body option 
+      * constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -196,7 +197,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path * constraints
+    With_module_body of identifier list * module_path 
+      * struct_expr_body option  * constraints
   | With_definition_body of  identifier list * constant_body
         
 and module_body = 
-- 
cgit v1.2.3