Inversion de l'ordre de chargement des objets logiques et non logiques

à la déclaration des paramètres de foncteurs (problème de
synchronisation révélé par bug #1118, apparu suite à l'appel de
lookup_mind par load_struct, suite au passage à un discharge local)

Les objets non logiques sont maintenant chargés après car ils peuvent
dépendre d'objets logiques. Et comme les objets non logiques
(p.ex. l'import récursif de modules dans la nametab) sont nécessaires
au typage de l'éventuelle contrainte de module, on reporte la gestion
de la contrainte au moment du end_module (on aurait peut-être pu faire
plus fin et extraire dans do_module la partie purement module, mais
après tout le report de la contrainte de type dans le end_module ne
semble pas génante).

À la date d'aujourd'hui, le bug #1118 reste toutefois ouvert avec les
définitions de module non interactives.


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

4 files changed, 10 insertions, 17 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index b20e7259d5..166b230077 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -41,7 +41,7 @@ let error_incompatible_labels l l' =
   error ("Opening and closing labels are not the same: "
 	 ^string_of_label l^" <> "^string_of_label l'^" !")
 
-let error_result_must_be_signature mtb = 
+let error_result_must_be_signature () = 
   error "The result module type must be a signature"
 
 let error_signature_expected mtb =
diff --git a/kernel/modops.mli b/kernel/modops.mli
index f102a5b2c0..b8f1f66a3c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -74,7 +74,7 @@ val error_incompatible_labels : label -> label -> 'a
 
 val error_no_such_label : label -> 'a
 
-val error_result_must_be_signature : module_type_body -> 'a
+val error_result_must_be_signature : unit -> 'a
 
 val error_signature_expected : module_type_body -> 'a
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9b638427cb..ca1bf6f65a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -30,7 +30,6 @@ type modvariant =
   | NONE 
   | SIG of (* funsig params *) (mod_bound_id * module_type_body) list 
   | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
-      * (* optional result type *) module_type_body option
   | LIBRARY of dir_path
 
 type module_info = 
@@ -224,7 +223,7 @@ let add_module l me senv =
 
 (* Interactive modules *)
 
-let start_module l params result senv = 
+let start_module l params senv = 
   check_label l senv.labset; 
   let rec trans_params env = function 
     | [] -> env,[] 
@@ -237,20 +236,13 @@ let start_module l params result senv =
 	env, (mbid,mtb)::transrest
   in
   let env,params_body = trans_params senv.env params in
-  let check_sig mtb = match scrape_modtype env mtb with
-    | MTBsig _ -> ()
-    | MTBfunsig _ -> error_result_must_be_signature mtb 
-    | _ -> anomaly "start_module: modtype not scraped"
-  in
-  let result_body = option_app (translate_modtype env) result in
-  ignore (option_app check_sig result_body);
   let msid = make_msid senv.modinfo.seed (string_of_label l) in
   let mp = MPself msid in
   let modinfo = { msid = msid;
 		  modpath = mp;
 		  seed = senv.modinfo.seed;
 		  label = l;
-		  variant = STRUCT(params_body,result_body) }
+		  variant = STRUCT params_body }
   in
   mp, { old = senv;
 	env = env;
@@ -263,13 +255,14 @@ let start_module l params result senv =
 
 
 
-let end_module l senv = 
+let end_module l restype senv = 
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
-  let params, restype = 
+  let restype = option_app (translate_modtype senv.env) restype in
+  let params = 
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
-      | STRUCT(params,restype) -> (params,restype)
+      | STRUCT params -> params
   in
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_local_context None;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5412287ee4..43755b9085 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -73,11 +73,11 @@ val set_engagement : engagement -> safe_environment -> safe_environment
 (*s Interactive module functions *)
 val start_module : 
   label -> (mod_bound_id * module_type_entry) list 
-    -> module_type_entry option 
       -> safe_environment -> module_path * safe_environment
 
 val end_module :
-  label -> safe_environment -> module_path * safe_environment 
+  label -> module_type_entry option 
+      -> safe_environment -> module_path * safe_environment 
 
 
 val start_modtype :