Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names

structure.

5 files changed, 87 insertions, 54 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 16803b3bf..0004f45a2 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -27,7 +27,7 @@ open Decls
 open Decl_kinds
 
 (** flag for internal message display *)
-type internal_flag = 
+type internal_flag =
   | UserAutomaticRequest (* kernel action, a message is displayed *)
   | InternalTacticRequest  (* kernel action, no message is displayed *)
   | UserIndividualRequest   (* user action, a message is displayed *)
@@ -63,7 +63,7 @@ let cache_variable ((sp,_),o) =
   add_variable_data id (p,opaq,ctx,poly,mk)
 
 let discharge_variable (_,o) = match o with
-  | Inr (id,_) -> 
+  | Inr (id,_) ->
     if variable_polymorphic id then None
     else Some (Inl (variable_context id))
   | Inl _ -> Some o
@@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) =
   Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = 
+let dummy_constant_entry =
   ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
@@ -185,7 +185,7 @@ let declare_constant_common id cst =
   Notation.declare_ref_arguments_scope (ConstRef c);
   c
 
-let definition_entry ?(opaque=false) ?(inline=false) ?types 
+let definition_entry ?(opaque=false) ?(inline=false) ?types
     ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body =
   { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
@@ -212,11 +212,11 @@ let declare_sideff env fix_exn se =
   in
   let ty_of cb =
     match cb.Declarations.const_type with
-    | Declarations.RegularArity t -> Some t 
+    | Declarations.RegularArity t -> Some t
     | Declarations.TemplateArity _ -> None in
   let cst_of cb pt =
     let pt, opaque = pt_opaque_of cb pt in
-    let univs, subst = 
+    let univs, subst =
       if cb.const_polymorphic then
 	let univs = Univ.instantiate_univ_context cb.const_universes in
 	  univs, Vars.subst_instance_constr (Univ.UContext.instance univs)
@@ -240,7 +240,7 @@ let declare_sideff env fix_exn se =
   } in
   let exists c =
     try ignore(Environ.lookup_constant c env); true
-    with Not_found -> false in 
+    with Not_found -> false in
   let knl =
     CList.map_filter (fun (c,cb,pt) ->
       if exists c then None
@@ -287,7 +287,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
 let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
-  let cb = 
+  let cb =
     definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
     declare_constant ~internal ~local id
@@ -383,12 +383,12 @@ let inInductive : inductive_obj -> obj =
 let declare_projections mind =
   let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
     match spec.mind_record with
-    | Some (Some (_, kns, pjs)) -> 
-      Array.iteri (fun i kn -> 
+    | Some (Some (_, kns, pjs)) ->
+      Array.iteri (fun i kn ->
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
 	let kn' = declare_constant id (ProjectionEntry entry,
-				       IsDefinition StructureComponent) 
+				       IsDefinition StructureComponent)
 	in
 	  assert(eq_constant kn kn')) kns; true
     | Some None | None -> false
@@ -442,52 +442,69 @@ let assumption_message id =
 
 (** Global universe names, in a different summary *)
 
-type universe_names = 
+type universe_names =
     (Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
 
-let input_universes : universe_names -> Libobject.obj =
-  let open Libobject in 
-    declare_object
-    { (default_object "Global universe name state") with
-      cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi);
-      load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi);
-      discharge_function = (fun (_, a) -> Some a);
-      classify_function = (fun a -> Keep a) }
+(* Discharged or not *)
+type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
 
-let do_universe l =
+let cache_universes (p, l) =
   let glob = Universes.global_universe_names () in
-  let glob', ctx = 
-    List.fold_left (fun ((idl,lid),ctx) (l, id) ->
-      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-        ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
-	 Univ.ContextSet.add_universe lev ctx))
+  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))
       (glob, Univ.ContextSet.empty) l
   in
     Global.push_context_set false ctx;
-    Lib.add_anonymous_leaf (input_universes glob')
+    if p then Lib.add_section_context ctx;
+    Universes.set_global_universe_names glob'
+
+let input_universes : universe_decl -> Libobject.obj =
+  declare_object
+    { (default_object "Global universe name state") with
+      cache_function = (fun (na, pi) -> cache_universes pi);
+      load_function = (fun _ (_, pi) -> cache_universes pi);
+      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+      classify_function = (fun a -> Keep a) }
+
+let do_universe poly l =
+  let l =
+    List.map (fun (l, id) ->
+	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
+	      (id, lev)) l
+  in
+    Lib.add_anonymous_leaf (input_universes (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 discharge_constraints (_, (p, c as a)) =
+  if p then None else Some a
 
-let input_constraints : Univ.constraints -> Libobject.obj =
-  let open Libobject in 
+let input_constraints : constraint_decl -> Libobject.obj =
+  let open Libobject in
     declare_object
     { (default_object "Global universe constraints") with
-      cache_function = (fun (na, c) -> Global.add_constraints c);
-      load_function = (fun _ (_, c) -> Global.add_constraints c);
-      discharge_function = (fun (_, a) -> Some a);
+      cache_function = cache_constraints;
+      load_function = (fun _ -> cache_constraints);
+      discharge_function = discharge_constraints;
       classify_function = (fun a -> Keep a) }
 
-let do_constraint l = 
-  let u_of_id = 
+let do_constraint poly l =
+  let u_of_id =
     let names, _ = Universes.global_universe_names () in
-      fun (loc, id) -> 
+      fun (loc, id) ->
 	try Idmap.find id names
 	with Not_found ->
-	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)	    
+	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
   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)
     Univ.Constraint.empty l
   in
-    Lib.add_anonymous_leaf (input_constraints constraints)
-  
+    Lib.add_anonymous_leaf (input_constraints (poly, constraints))
diff --git a/library/declare.mli b/library/declare.mli
index 76538a624..7ed451c3f 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -85,5 +85,5 @@ val exists_name : Id.t -> bool
 
 (** Global universe names and constraints *)
 
-val do_universe : Id.t Loc.located list -> unit
-val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_universe : polymorphic -> Id.t Loc.located list -> unit
+val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
diff --git a/library/lib.ml b/library/lib.ml
index f4f52db53..cdc888903 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -392,10 +392,13 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
 		  
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
+type secentry =
+  | Variable of (Names.Id.t * Decl_kinds.binding_kind *
+		   Decl_kinds.polymorphic * Univ.universe_context_set)
+  | Context of Univ.universe_context_set
+
 let sectab =
-  Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * 
-		Decl_kinds.polymorphic * Univ.universe_context_set) list *
-		        Opaqueproof.work_list * abstr_list) list)
+  Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list)
     ~name:"section-context"
 
 let add_section () =
@@ -406,21 +409,29 @@ let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl
+	sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+
+let add_section_context ctx =
+  match !sectab with
+    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
+    | (vars,repl,abs)::sl ->
+	sectab := (Context ctx :: vars,repl,abs)::sl
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
+    | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
       let l, r = aux (idl,hyps) in 
 	(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
-    | ((_,_,poly,ctx)::idl,hyps) -> 
+    | (Variable (_,_,poly,ctx)::idl,hyps) ->
         let l, r = aux (idl,hyps) in
           l, if poly then Univ.ContextSet.union r ctx else r
+    | (Context ctx :: idl, hyps) ->
+       let l, r = aux (idl, hyps) in
+       l, Univ.ContextSet.union r ctx
     | [], _ -> [],Univ.ContextSet.empty
   in aux (secs,ohyps)
 
 let instance_from_variable_context sign =
-
   let rec inst_rec = function
     | (id,b,None,_) :: sign -> id :: inst_rec sign
     | _ :: sign -> inst_rec sign
@@ -437,7 +448,8 @@ let add_section_replacement f g hyps =
     let ctx = Univ.ContextSet.to_context ctx in
     let subst, ctx = Univ.abstract_universes true ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl
+    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
+	      g (sechyps,subst,ctx) abs)::sl
 
 let add_section_kn kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -457,10 +469,13 @@ let section_segment_of_mutual_inductive kn =
 
 let section_instance = function
   | VarRef id ->
-      if List.exists (fun (id',_,_,_) -> Names.id_eq id id') 
-	(pi1 (List.hd !sectab))
-      then Univ.Instance.empty, [||]
-      else raise Not_found
+     let eq = function
+       | Variable (id',_,_,_) -> Names.id_eq id id'
+       | Context _ -> false
+     in
+     if List.exists eq (pi1 (List.hd !sectab))
+     then Univ.Instance.empty, [||]
+     else raise Not_found
   | ConstRef con ->
       Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
diff --git a/library/lib.mli b/library/lib.mli
index 9c4d26c5b..b67b2b873 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -172,7 +172,7 @@ val section_instance : Globnames.global_reference -> Univ.universe_instance * Na
 val is_in_section : Globnames.global_reference -> bool
 
 val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
-
+val add_section_context : Univ.universe_context_set -> unit
 val add_section_constant : bool (* is_projection *) -> 
   Names.constant -> Context.named_context -> unit
 val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit
diff --git a/library/universes.ml b/library/universes.ml
index 0656188eb..30d38eb2a 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -16,7 +16,8 @@ open Univ
 type universe_names = 
     Univ.universe_level Idmap.t * Id.t Univ.LMap.t
 
-let global_universes = Summary.ref ~name:"Global universe names" 
+let global_universes =
+  Summary.ref ~name:"Global universe names"
   ((Idmap.empty, Univ.LMap.empty) : universe_names)
 
 let global_universe_names () = !global_universes