Univs: more robust Universe/Constraint decls #4816

This fixes the declarations of constraints, universes
and assumptions:
- global constraints can refer to global universes only,
- polymorphic universes, constraints and assumptions can only be
  declared inside sections, when all the section's
  variables/universes are polymorphic as well.
- monomorphic assumptions may only be declared in section contexts
  which are not parameterized by polymorphic universes/assumptions.

Add fix for part 1 of bug #4816

3 files changed, 34 insertions, 10 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b0df32b8de..84284fd182 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -440,8 +440,9 @@ let cache_universes (p, l) =
   let glob = Universes.global_universe_names () in
   let glob', ctx =
     List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
-		    ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
-		     Univ.ContextSet.add_universe lev ctx))
+        ((Idmap.add id (p, lev) idl,
+          Univ.LMap.add lev id lid),
+         Univ.ContextSet.add_universe lev ctx))
       (glob, Univ.ContextSet.empty) l
   in
     Global.push_context_set p ctx;
@@ -457,6 +458,12 @@ let input_universes : universe_decl -> Libobject.obj =
       classify_function = (fun a -> Keep a) }
 
 let do_universe poly l =
+  let in_section = Lib.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      user_err_loc (Loc.ghost, "Constraint",
+                    str"Cannot declare polymorphic universes outside sections")
+  in
   let l =
     List.map (fun (l, id) ->
 	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
@@ -485,14 +492,30 @@ let input_constraints : constraint_decl -> Libobject.obj =
 let do_constraint poly l =
   let u_of_id =
     let names, _ = Universes.global_universe_names () in
-      fun (loc, id) ->
-	try Idmap.find id names
-	with Not_found ->
-	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+    fun (loc, id) ->
+    try Idmap.find id names
+    with Not_found ->
+      user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+  in
+  let in_section = Lib.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      user_err_loc (Loc.ghost, "Constraint",
+                    str"Cannot declare polymorphic constraints outside sections")
+  in
+  let check_poly loc p loc' p' =
+    if poly then ()
+    else if p || p' then
+      let loc = if p then loc else loc' in
+      user_err_loc (loc, "Constraint",
+                    str "Cannot declare a global constraint on " ++
+                    str "a polymorphic universe, use "
+                    ++ str "Polymorphic Constraint instead")
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
-    let lu = u_of_id l and ru = u_of_id r in
-      Univ.Constraint.add (lu, d, ru) acc)
+     let p, lu = u_of_id l and p', ru = u_of_id r in
+     check_poly (fst l) p (fst r) p';
+     Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
   in
     Lib.add_anonymous_leaf (input_constraints (poly, constraints))
diff --git a/library/universes.ml b/library/universes.ml
index c4eb2afcbb..75cbd5604b 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -13,10 +13,11 @@ open Term
 open Environ
 open Univ
 open Globnames
+open Decl_kinds
 
 (** Global universe names *)
 type universe_names = 
-    Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+  (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
 
 let global_universes =
   Summary.ref ~name:"Global universe names"
diff --git a/library/universes.mli b/library/universes.mli
index 53cf5f3844..a5740ec49f 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -19,7 +19,7 @@ val is_set_minimization : unit -> bool
 
 (** Global universe name <-> level mapping *)
 type universe_names = 
-  Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+  (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
 
 val global_universe_names : unit -> universe_names
 val set_global_universe_names : universe_names -> unit