1 files changed, 76 insertions, 26 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 5f6f0fe4..c9992fff 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -9,7 +9,7 @@
 (** This module is about the low-level declaration of logical objects *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Libnames
@@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) =
       obj.cst_was_seff <- false;  
       if Global.exists_objlabel (Label.of_id (basename sp))
       then constant_of_kn kn
-      else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
     end else
       let () = check_exists sp in
       let kn', exported = Global.add_constant dir id obj.cst_decl in
@@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) =
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant (cst.const_proj <> None) kn' cst.const_hyps;
+  add_section_constant cst.const_polymorphic kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
   add_constant_kind (constant_of_kn kn) obj.cst_kind
 
@@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let kn' = Global.add_mind dir id mie in
   assert (eq_mind kn' (mind_of_kn kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn kn' mind.mind_hyps;
+  add_section_kn mind.mind_polymorphic kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
@@ -353,7 +353,8 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
   mind_entry_universes = Univ.UContext.empty;
-  mind_entry_private = None })
+  mind_entry_private = None;
+})
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
@@ -398,7 +399,7 @@ let declare_mind mie =
 let pr_rank i = pr_nth (i+1)
 
 let fixpoint_message indexes l =
-  Flags.if_verbose msg_info (match l with
+  Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "no recursive definition")
   | [id] -> pr_id id ++ str " is recursively defined" ++
       (match indexes with
@@ -413,7 +414,7 @@ let fixpoint_message indexes l =
 		    | None -> mt ()))
 
 let cofixpoint_message l =
-  Flags.if_verbose msg_info (match l with
+  Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "No corecursive definition.")
   | [id] -> pr_id id ++ str " is corecursively defined"
   | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
@@ -423,15 +424,32 @@ let recursive_message isfix i l =
   (if isfix then fixpoint_message i else cofixpoint_message) l
 
 let definition_message id =
-  Flags.if_verbose msg_info (pr_id id ++ str " is defined")
+  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
 
 let assumption_message id =
-  Flags.if_verbose msg_info (pr_id id ++ str " is assumed")
+  (* Changing "assumed" to "declared", "assuming" referring more to
+  the type of the object than to the name of the object (see
+  discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
+  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
 
 (** Global universe names, in a different summary *)
 
-type universe_names =
-    (Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
+type universe_context_decl = polymorphic * Univ.universe_context_set
+
+let cache_universe_context (p, ctx) =
+  Global.push_context_set p ctx;
+  if p then Lib.add_section_context ctx
+
+let input_universe_context : universe_context_decl -> Libobject.obj =
+  declare_object
+    { (default_object "Global universe context state") with
+      cache_function = (fun (na, pi) -> cache_universe_context pi);
+      load_function = (fun _ (_, pi) -> cache_universe_context pi);
+      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+      classify_function = (fun a -> Keep a) }
+
+let declare_universe_context poly ctx =
+  Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
 
 (* Discharged or not *)
 type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
@@ -440,13 +458,13 @@ 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;
-    if p then Lib.add_section_context ctx;
-    Universes.set_global_universe_names glob'
+  cache_universe_context (p, ctx);
+  Universes.set_global_universe_names glob'
 
 let input_universes : universe_decl -> Libobject.obj =
   declare_object
@@ -457,6 +475,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
@@ -467,8 +491,10 @@ let do_universe poly l =
 type constraint_decl = polymorphic * Univ.constraints
 
 let cache_constraints (na, (p, c)) =
-  Global.add_constraints c;
-  if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)
+  let ctx =
+    Univ.ContextSet.add_constraints c
+      Univ.ContextSet.empty (* No declared universes here, just constraints *)
+  in cache_universe_context (p,ctx)
 
 let discharge_constraints (_, (p, c as a)) =
   if p then None else Some a
@@ -483,16 +509,40 @@ let input_constraints : constraint_decl -> Libobject.obj =
       classify_function = (fun a -> Keep a) }
 
 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)
+  let open Misctypes in
+  let u_of_id x =
+    match x with
+    | GProp -> Loc.dummy_loc, (false, Univ.Level.prop)
+    | GSet -> Loc.dummy_loc, (false, Univ.Level.set)
+    | GType None ->
+       user_err_loc (Loc.dummy_loc, "Constraint",
+                     str "Cannot declare constraints on anonymous universes")
+    | GType (Some (loc, id)) ->
+       let id = Id.of_string id in
+       let names, _ = Universes.global_universe_names () in
+       try loc, 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 ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
+     check_poly ploc p rloc p';
+     Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
   in
     Lib.add_anonymous_leaf (input_constraints (poly, constraints))