bug in safe_typing: univ constraints generated by section variables were not stored in modules

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

1 files changed, 43 insertions, 3 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index efc2fa8658..d65caf7cab 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -42,6 +42,11 @@ type module_info =
 let check_label l labset = 
   if Labset.mem l labset then error_existing_label l
 
+let set_engagement_opt oeng env =
+  match oeng with
+      Some eng -> set_engagement eng env
+    | _ -> env
+
 type library_info = dir_path * Digest.t
 
 type safe_environment = 
@@ -51,6 +56,8 @@ type safe_environment =
       labset : Labset.t;
       revsign : module_signature_body;
       revstruct : module_structure_body;
+      univ : Univ.constraints;
+      engagement : engagement option;
       imports : library_info list;
       loads : (module_path * module_body) list;
       local_retroknowledge : Retroknowledge.action list}
@@ -79,6 +86,8 @@ let rec empty_environment =
     labset = Labset.empty;
     revsign = [];
     revstruct = [];
+    univ = Univ.Constraint.empty;
+    engagement = None;
     imports = [];
     loads = [];
     local_retroknowledge = [] }
@@ -207,6 +216,8 @@ let add_constant dir l decl senv =
 	  labset = Labset.add l senv.labset;
 	  revsign = (l,SPBconst cb)::senv.revsign;
 	  revstruct = (l,SEBconst cb)::senv.revstruct;
+          univ = senv.univ;
+          engagement = senv.engagement;
 	  imports = senv.imports;
 	  loads = senv.loads ;
 	  local_retroknowledge = senv.local_retroknowledge }
@@ -235,6 +246,8 @@ let add_mind dir l mie senv =
 	labset = Labset.add l senv.labset;  (* TODO: the same as above *)
 	revsign = (l,SPBmind mib)::senv.revsign;
 	revstruct = (l,SEBmind mib)::senv.revstruct;
+        univ = senv.univ;
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads;
         local_retroknowledge = senv.local_retroknowledge }
@@ -254,6 +267,8 @@ let add_modtype l mte senv =
 	labset = Labset.add l senv.labset;
 	revsign = (l,SPBmodtype mtb)::senv.revsign;
 	revstruct = (l,SEBmodtype mtb)::senv.revstruct;
+        univ = senv.univ;
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads;
         local_retroknowledge = senv.local_retroknowledge }
@@ -279,6 +294,8 @@ let add_module l me senv =
 	labset = Labset.add l senv.labset;
 	revsign = (l,SPBmodule mspec)::senv.revsign;
 	revstruct = (l,SEBmodule mb)::senv.revstruct;
+        univ = senv.univ;
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads;
         local_retroknowledge = senv.local_retroknowledge }
@@ -302,6 +319,8 @@ let start_module l senv =
 	labset = Labset.empty;
 	revsign = [];
 	revstruct = [];
+        univ = Univ.Constraint.empty;
+        engagement = None;
 	imports = senv.imports;
 	loads = [];
 	(* spiwack : not sure, but I hope it's correct *)
@@ -333,6 +352,7 @@ let end_module l restype senv =
 	  let mtb = functorize_type res_tb in
 	    mtb, Some mtb, cst
   in
+  let cst = Constraint.union cst senv.univ in
   let mexpr = 
     List.fold_left
       (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb))
@@ -354,6 +374,7 @@ let end_module l restype senv =
   in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
+  let newenv = set_engagement_opt senv.engagement newenv in
   let newenv = 
     List.fold_left
       (fun env (mp,mb) -> full_add_module mp mb env) 
@@ -369,6 +390,9 @@ let end_module l restype senv =
 	labset = Labset.add l oldsenv.labset;
 	revsign = (l,SPBmodule mspec)::oldsenv.revsign;
 	revstruct = (l,SEBmodule mb)::oldsenv.revstruct;
+        univ = oldsenv.univ;
+        (* engagement is propagated to the upper level *)
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads@oldsenv.loads;
 	local_retroknowledge = senv.local_retroknowledge@oldsenv.local_retroknowledge }
@@ -394,6 +418,8 @@ let add_module_parameter mbid mte senv =
     labset = senv.labset;
     revsign = [];
     revstruct = [];
+    univ = senv.univ;
+    engagement = senv.engagement;
     imports = senv.imports;
     loads = [];
     local_retroknowledge = senv.local_retroknowledge }
@@ -417,6 +443,8 @@ let start_modtype l senv =
 	labset = Labset.empty;
 	revsign = [];
 	revstruct = [];
+        univ = Univ.Constraint.empty;
+        engagement = None;
 	imports = senv.imports;
 	loads = [];
 	(* spiwack: not 100% sure, but I think it should be like that *)
@@ -441,6 +469,10 @@ let end_modtype l senv =
   in
   let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in
   let newenv = oldsenv.env in
+  (* since universes constraints cannot be stored in the modtype,
+     they are propagated to the upper level *)
+  let newenv = add_constraints senv.univ  newenv in
+  let newenv = set_engagement_opt senv.engagement newenv in
   let newenv = 
     List.fold_left
       (fun env (mp,mb) -> full_add_module mp mb env) 
@@ -459,6 +491,8 @@ let end_modtype l senv =
 	labset = Labset.add l oldsenv.labset;
 	revsign = (l,SPBmodtype mtb)::oldsenv.revsign;
 	revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct;
+        univ = Univ.Constraint.union senv.univ oldsenv.univ;
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads@oldsenv.loads;
         (* spiwack : if there is a bug with retroknowledge in nested modules
@@ -472,7 +506,9 @@ let current_msid senv = senv.modinfo.msid
 
 
 let add_constraints cst senv = 
-  {senv with env = Environ.add_constraints cst senv.env}
+  {senv with
+    env = Environ.add_constraints cst senv.env;
+    univ = Univ.Constraint.union cst senv.univ }
 
 (* Check that the engagement expected by a library matches the initial one *)
 let check_engagement env c =
@@ -483,7 +519,9 @@ let check_engagement env c =
         error "Needs option -impredicative-set"
 
 let set_engagement c senv =
-  {senv with env = Environ.set_engagement c senv.env}
+  {senv with
+    env = Environ.set_engagement c senv.env;
+    engagement = Some c }
 
 (* Libraries = Compiled modules *)
 
@@ -521,6 +559,8 @@ let start_library dir senv =
 	labset = Labset.empty;
 	revsign = [];
 	revstruct = [];
+        univ = Univ.Constraint.empty;
+        engagement = None;
 	imports = senv.imports;
 	loads = [];
         local_retroknowledge = [] }
@@ -545,7 +585,7 @@ let export senv dir =
       mod_type = MTBsig (modinfo.msid, List.rev senv.revsign);
       mod_user_type = None;
       mod_equiv = None;
-      mod_constraints = Constraint.empty;
+      mod_constraints = senv.univ;
       mod_retroknowledge = senv.local_retroknowledge}
   in
     modinfo.msid, (dir,mb,senv.imports,engagement senv.env)