Module type expressions of the form (Fsig X) with Definition foo := bar are now accepted.

+svn:ignore property on folders



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12429 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 5 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 48928470a..26ad7e383 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -50,14 +50,18 @@ let rec rebuild_mp mp l =
     | i::r -> rebuild_mp (MPdot(mp,i)) r 
 	
 let rec check_with env sign with_decl alg_sign mp equiv = 
-  match with_decl with
+  let sign,wd,equiv,cst= match with_decl with
     | With_Definition (id,_) ->
 	let sign,cb,cst = check_with_aux_def env sign with_decl mp equiv in
-	  sign,Some (SEBwith(alg_sign,With_definition_body(id,cb))),equiv,cst
+	  sign,With_definition_body(id,cb),equiv,cst
     | With_Module (id,mp1) -> 
 	let sign,equiv,cst = 
 	  check_with_aux_mod env sign with_decl mp equiv in
-	  sign,Some (SEBwith(alg_sign,With_module_body(id,mp1))),equiv,cst
+	  sign,With_module_body(id,mp1),equiv,cst in
+    if alg_sign = None then
+      sign,None,equiv,cst
+    else
+      sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
 	    
 and check_with_aux_def env sign with_decl mp equiv = 
   let sig_b = match sign with 
@@ -299,7 +303,7 @@ and translate_struct_module_entry env mp mse  = match mse with
       Univ.Constraint.union cst1 cst
   | MSEwith(mte, with_decl) ->
       let sign,alg,resolve,cst1 = translate_struct_module_entry env mp mte in
-      let sign,alg,resolve,cst2 = check_with env sign with_decl alg mp resolve in
+      let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in
 	sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2
 	  
 and translate_struct_type_entry env mse  = match mse with
@@ -335,7 +339,7 @@ and translate_struct_type_entry env mse  = match mse with
   | MSEwith(mte, with_decl) ->
       let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in
       let sign,alg,resolve,cst1 = 
-	check_with env sign with_decl (Option.get alg) mp_from resolve in
+	check_with env sign with_decl alg mp_from resolve in
 	sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1    
 
 and translate_module_type env mp mte =