fixed universes bug related to module inclusion

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

4 files changed, 60 insertions, 10 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 1b2147d28..662841cdf 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -315,3 +315,49 @@ and add_module_constraints env mb =
 and add_modtype_constraints env mtb = 
   add_struct_expr_constraints env mtb.typ_expr
       
+
+let rec struct_expr_constraints cst = function
+  | SEBident _ -> cst
+
+  | SEBfunctor (_,mtb,meb) -> 
+      struct_expr_constraints 
+	(modtype_constraints cst mtb) meb
+
+  | SEBstruct (_,structure_body) ->
+      List.fold_left 
+        (fun cst (l,item) -> struct_elem_constraints cst item)
+        cst
+        structure_body
+
+  | SEBapply (meb1,meb2,cst1) ->
+      struct_expr_constraints 
+	(struct_expr_constraints (Univ.Constraint.union cst1 cst) meb1)
+	meb2
+  | SEBwith(meb,With_definition_body(_,cb))->
+      struct_expr_constraints
+        (Univ.Constraint.union cb.const_constraints cst) meb
+  | SEBwith(meb,With_module_body(_,_,cst1))->
+      struct_expr_constraints (Univ.Constraint.union cst1 cst) meb	
+		
+and struct_elem_constraints cst = function 
+  | SFBconst cb -> cst
+  | SFBmind mib -> cst
+  | SFBmodule mb -> module_constraints cst mb
+  | SFBalias (mp,Some cst1) -> Univ.Constraint.union cst1 cst
+  | SFBalias (mp,None) -> cst
+  | SFBmodtype mtb -> modtype_constraints cst mtb
+
+and module_constraints cst mb = 
+  let cst = match mb.mod_expr with
+    | None -> cst
+    | Some meb -> struct_expr_constraints cst meb in
+  let cst = match mb.mod_type with
+    | None -> cst
+    | Some mtb -> struct_expr_constraints cst mtb in
+  Univ.Constraint.union mb.mod_constraints cst
+
+and modtype_constraints cst mtb = 
+  struct_expr_constraints cst mtb.typ_expr
+      
+
+let struct_expr_constraints = struct_expr_constraints Univ.Constraint.empty
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index e3045555f..eb7dbe994 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -27,3 +27,5 @@ val add_module_constraints : env -> module_body -> env
 
 val add_struct_expr_constraints : env -> struct_expr_body -> env
 
+val struct_expr_constraints : struct_expr_body -> Univ.constraints
+
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2fffa0922..35bb1267a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -251,6 +251,12 @@ let add_mind dir l mie senv =
 	loads = senv.loads;
         local_retroknowledge = senv.local_retroknowledge }
 
+(* Insertion of orphaned universe constraints *)
+
+let add_constraints cst senv = 
+  {senv with
+    env = Environ.add_constraints cst senv.env;
+    univ = Univ.Constraint.union cst senv.univ }
 
 (* Insertion of module types *)
 
@@ -434,7 +440,7 @@ let end_module l restype senv =
 (* Include for module and module type*)
  let add_include me senv =
    let struct_expr,_ =  translate_struct_entry senv.env me in
-   let senv = { senv with env = add_struct_expr_constraints senv.env struct_expr } in
+   let senv = add_constraints (struct_expr_constraints struct_expr) senv in
    let msid,str = match (eval_struct senv.env struct_expr) with
      | SEBstruct(msid,str_l) -> msid,str_l
      | _ -> error ("You cannot Include a higher-order Module or Module Type" )
@@ -603,7 +609,7 @@ let end_modtype l senv =
   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 = Environ.add_constraints senv.univ  newenv in
   let newenv = set_engagement_opt senv.engagement newenv in
   let newenv = 
     List.fold_left
@@ -640,11 +646,6 @@ let current_modpath senv = senv.modinfo.modpath
 let current_msid senv = senv.modinfo.msid
 
 
-let add_constraints cst senv = 
-  {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 =
   match Environ.engagement env, c with
diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v
index fd17457f0..4be70d888 100644
--- a/test-suite/failure/univ_include.v
+++ b/test-suite/failure/univ_include.v
@@ -17,13 +17,14 @@ Module G (E : MU).
   Include F E.
 Print Universes. (* U <= T *)
 End G.
-Print Universes. (* constraint lost! *)
+Print Universes. (* Check if constraint is lost *)
 
 Module Mt.
-  Definition t :=T.
+  Definition t := T.
 End Mt.
 
-Module P := G Mt.
+Module P := G Mt. (* should yield Universe inconsistency *)
+(* ... otherwise the following command will show that T has type T! *)
 Eval cbv delta [P.elt Mt.t] in P.elt.