From ed7af646f2e486b7e96812ba2335e644756b70fd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 27 Oct 2015 13:55:45 -0400
Subject: Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names
 structure.

---
 library/declare.ml   | 93 +++++++++++++++++++++++++++++++---------------------
 library/declare.mli  |  4 +--
 library/lib.ml       | 39 +++++++++++++++-------
 library/lib.mli      |  2 +-
 library/universes.ml |  3 +-
 5 files changed, 87 insertions(+), 54 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 16803b3bfa..0004f45a29 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 76538a6248..7ed451c3f1 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 f4f52db53b..cdc8889037 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 9c4d26c5b2..b67b2b873f 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 0656188eb5..30d38eb2a4 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
-- 
cgit v1.2.3


From 0a1b046d37761fe47435d5041bb5031e3f7d6613 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 28 Oct 2015 10:03:17 +0100
Subject: lib_stack: API to reorder the libstack

For discharging it is important that constants occur in the libstack
in an order that respects the dependencies among them.  This is
impossible to achieve for private constants when they are exported globally
without this (ugly IMO) api.
---
 library/lib.ml  | 3 +++
 library/lib.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index cdc8889037..297441e6e2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -198,6 +198,9 @@ let split_lib_at_opening sp =
 let add_entry sp node =
   lib_stk := (sp,node) :: !lib_stk
 
+let pull_to_head oname =
+  lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk
+
 let anonymous_id =
   let n = ref 0 in
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
diff --git a/library/lib.mli b/library/lib.mli
index b67b2b873f..bb88317591 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -55,6 +55,7 @@ val segment_of_objects :
 
 val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
 val add_anonymous_leaf : Libobject.obj -> unit
+val pull_to_head : Libnames.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
-- 
cgit v1.2.3


From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 28 Oct 2015 16:46:42 +0100
Subject: Avoid type checking private_constants (side_eff) again during Qed
 (#4357).

Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing.  When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined.  Only when the
comparison is successful the private_constant is not re-checked.  Otherwise
else it is.  In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.

Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron).  Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
---
 library/declare.ml   | 151 +++++++++++++++++++++------------------------------
 library/declare.mli  |  10 ++--
 library/global.mli   |   5 +-
 library/heads.ml     |   5 +-
 library/libobject.ml |   3 +
 5 files changed, 78 insertions(+), 96 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 0004f45a29..63e5a72245 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -35,7 +35,7 @@ type internal_flag =
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
-  | SectionLocalDef of definition_entry
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -93,9 +93,13 @@ type constant_obj = {
   cst_hyps : Dischargedhypsmap.discharged_hyps;
   cst_kind : logical_kind;
   cst_locl : bool;
+  mutable cst_exported : Safe_typing.exported_private_constant list;
+  (* mutable: to avoid change the libobject API, since cache_function
+   * does not return an updated object *)
+  mutable cst_was_seff : bool
 }
 
-type constant_declaration = constant_entry * logical_kind
+type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
@@ -131,8 +135,17 @@ let check_exists sp =
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  let () = check_exists sp in
-  let kn' = Global.add_constant dir id obj.cst_decl in
+  let kn' =
+    if obj.cst_was_seff then begin
+      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))
+    end else
+      let () = check_exists sp in
+      let kn', exported = Global.add_constant dir id obj.cst_decl in
+      obj.cst_exported <- exported;
+      kn' in
   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
@@ -156,20 +169,23 @@ 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 =
-  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+let dummy_constant_entry = 
+  ConstantEntry
+    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
   cst_hyps = [];
   cst_kind = cst.cst_kind;
   cst_locl = cst.cst_locl;
+  cst_exported = [];
+  cst_was_seff = cst.cst_was_seff;
 }
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let inConstant : constant_obj -> obj =
-  declare_object { (default_object "CONSTANT") with
+let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
+  declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -177,16 +193,40 @@ let inConstant : constant_obj -> obj =
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
 
+let declare_scheme = ref (fun _ _ -> assert false)
+let set_declare_scheme f = declare_scheme := f
+
 let declare_constant_common id cst =
-  let (sp,kn) = add_leaf id (inConstant cst) in
+  let update_tables c =
+(*  Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
+    declare_constant_implicits c;
+    Heads.declare_head (EvalConstRef c);
+    Notation.declare_ref_arguments_scope (ConstRef c) in
+  let o = inConstant cst in
+  let _, kn as oname = add_leaf id o in
+  List.iter (fun (c,ce,role) ->
+      (* handling of private_constants just exported *)
+      let o = inConstant {
+        cst_decl = ConstantEntry (false, ce);
+        cst_hyps = [] ;
+        cst_kind = IsProof Theorem;
+        cst_locl = false;
+        cst_exported = [];
+        cst_was_seff = true; } in
+      let id = Label.to_id (pi3 (Constant.repr3 c)) in
+      ignore(add_leaf id o);
+      update_tables c;
+      match role with
+      | Safe_typing.Subproof -> ()
+      | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|])
+    (outConstant o).cst_exported;
+  pull_to_head oname;
   let c = Global.constant_of_delta_kn kn in
-  declare_constant_implicits c;
-  Heads.declare_head (EvalConstRef c);
-  Notation.declare_ref_arguments_scope (ConstRef c);
+  update_tables c;
   c
 
 let definition_entry ?(opaque=false) ?(inline=false) ?types
-    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body =
+    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
   { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
@@ -196,90 +236,25 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let declare_scheme = ref (fun _ _ -> assert false)
-let set_declare_scheme f = declare_scheme := f
-let declare_sideff env fix_exn se =
-  let cbl, scheme = match se with
-    | SEsubproof (c, cb, pt) -> [c, cb, pt], None
-    | SEscheme (cbl, k) ->
-        List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in
-  let id_of c = Names.Label.to_id (Names.Constant.label c) in
-  let pt_opaque_of cb pt =
-    match cb, pt with
-    | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false
-    | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true
-    | _ -> assert false
-  in
-  let ty_of cb =
-    match cb.Declarations.const_type with
-    | 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 =
-      if cb.const_polymorphic then
-	let univs = Univ.instantiate_univ_context cb.const_universes in
-	  univs, Vars.subst_instance_constr (Univ.UContext.instance univs)
-      else cb.const_universes, fun x -> x
-    in
-    let pt = (subst (fst pt), snd pt) in
-    let ty = Option.map subst (ty_of cb) in
-    { cst_decl = ConstantEntry (DefinitionEntry {
-        const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff);
-        const_entry_secctx = Some cb.Declarations.const_hyps;
-        const_entry_type = ty;
-        const_entry_opaque = opaque;
-        const_entry_inline_code = false;
-        const_entry_feedback = None;
-	const_entry_polymorphic = cb.const_polymorphic;
-	const_entry_universes = univs;
-    });
-    cst_hyps = [] ;
-    cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
-    cst_locl = true;
-  } in
-  let exists c =
-    try ignore(Environ.lookup_constant c env); true
-    with Not_found -> false in
-  let knl =
-    CList.map_filter (fun (c,cb,pt) ->
-      if exists c then None
-      else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in
-  match scheme with
-  | None -> ()
-  | Some (inds_consts,kind) ->
-      !declare_scheme kind (Array.of_list
-         (List.map (fun (c,kn) ->
-             CList.find_map (fun (x,c',_,_) ->
-               if Constant.equal c c' then Some (x,kn) else None) inds_consts)
-           knl))
-
 let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
-  let cd = (* We deal with side effects *)
+  let export = (* We deal with side effects *)
     match cd with
-    | Entries.DefinitionEntry de ->
-        if export_seff ||
-           not de.const_entry_opaque ||
-           de.const_entry_polymorphic then
+    | DefinitionEntry de when
+        export_seff ||
+        not de.const_entry_opaque ||
+        de.const_entry_polymorphic ->
           let bo = de.const_entry_body in
           let _, seff = Future.force bo in
-          if Declareops.side_effects_is_empty seff then cd
-          else begin
-            let seff = Declareops.uniquize_side_effects seff in
-            Declareops.iter_side_effects
-              (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
-            Entries.DefinitionEntry { de with
-              const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
-                pt, Declareops.no_seff) }
-        end
-        else cd
-    | _ -> cd
+          Safe_typing.empty_private_constants <> seff
+    | _ -> false
   in
   let cst = {
-    cst_decl = ConstantEntry cd;
+    cst_decl = ConstantEntry (export,cd);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
+    cst_exported = [];
+    cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
   kn
diff --git a/library/declare.mli b/library/declare.mli
index 7ed451c3f1..fdbd235614 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -22,7 +22,7 @@ open Decl_kinds
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of definition_entry
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -32,7 +32,7 @@ val declare_variable : variable -> variable_declaration -> object_name
 (** Declaration of global constructions 
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = constant_entry * logical_kind
+type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
@@ -49,8 +49,8 @@ type internal_flag =
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
-  ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects ->
-  constr -> definition_entry
+  ?poly:polymorphic -> ?univs:Univ.universe_context ->
+  ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 val declare_constant :
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
@@ -60,7 +60,7 @@ val declare_definition :
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
 
-(** Since transparent constant's side effects are globally declared, we
+(** Since transparent constants' side effects are globally declared, we
  *  need that *)
 val set_declare_scheme :
   (string -> (inductive * constant) array -> unit) -> unit
diff --git a/library/global.mli b/library/global.mli
index ac231f7fd8..03469bea41 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,10 +31,11 @@ val set_engagement : Declarations.engagement -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Entries.definition_entry) -> Univ.universe_context_set
+val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
 
 val add_constant :
-  DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
+  DirPath.t -> Id.t -> Safe_typing.global_declaration ->
+    constant * Safe_typing.exported_private_constant list
 val add_mind :
   DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
 
diff --git a/library/heads.ml b/library/heads.ml
index 5c153b0676..73d2aa053f 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -68,7 +68,10 @@ let kind_of_head env t =
         | None -> NotImmediatelyComputableHead)
   | Const (cst,_) ->
       (try on_subterm k l b (constant_head cst)
-       with Not_found -> assert false)
+       with Not_found ->
+         Errors.anomaly
+           Pp.(str "constant not found in kind_of_head: " ++
+               str (Names.Constant.to_string cst)))
   | Construct _ | CoFix _ ->
       if b then NotImmediatelyComputableHead else ConstructorHead
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
diff --git a/library/libobject.ml b/library/libobject.ml
index 2ee57baf9c..85c830ea2c 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -108,6 +108,9 @@ let declare_object_full odecl =
 let declare_object odecl =
   try fst (declare_object_full odecl)
   with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
+let declare_object_full odecl =
+  try declare_object_full odecl
+  with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
 
 let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
 
-- 
cgit v1.2.3


From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Oct 2015 12:36:20 -0400
Subject: Univs: local names handling.

Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
---
 library/universes.ml  | 16 ++++++++++++++++
 library/universes.mli | 10 +++++++++-
 2 files changed, 25 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/universes.ml b/library/universes.ml
index 30d38eb2a4..6cccb10efb 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -12,7 +12,9 @@ open Names
 open Term
 open Environ
 open Univ
+open Globnames
 
+(** Global universe names *)
 type universe_names = 
     Univ.universe_level Idmap.t * Id.t Univ.LMap.t
 
@@ -27,6 +29,20 @@ let pr_with_global_universes l =
   try Nameops.pr_id (LMap.find l (snd !global_universes))
   with Not_found -> Level.pr l
 
+(** Local universe names of polymorphic references *)
+
+type universe_binders = (Id.t * Univ.universe_level) list
+
+let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+
+let universe_binders_of_global ref =
+  try
+    let l = Refmap.find ref !universe_binders_table in l
+  with Not_found -> []
+
+let register_universe_binders ref l =
+  universe_binders_table := Refmap.add ref l !universe_binders_table
+		     
 (* To disallow minimization to Set *)
 
 let set_minimization = ref true
diff --git a/library/universes.mli b/library/universes.mli
index 4ff21d45c9..45672ef460 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -14,9 +14,10 @@ open Univ
 
 val set_minimization : bool ref
 val is_set_minimization : unit -> bool
-       
+
 (** Universes *)
 
+(** Global universe name <-> level mapping *)
 type universe_names = 
   Univ.universe_level Idmap.t * Id.t Univ.LMap.t
 
@@ -25,6 +26,13 @@ val set_global_universe_names : universe_names -> unit
 
 val pr_with_global_universes : Level.t -> Pp.std_ppcmds
 
+(** Local universe name <-> level mapping *)
+
+type universe_binders = (Id.t * Univ.universe_level) list
+					   
+val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
+val universe_binders_of_global : Globnames.global_reference -> universe_binders
+
 (** The global universe counter *)
 val set_remote_new_univ_level : universe_level RemoteCounter.installer
 
-- 
cgit v1.2.3