Merge PR #890: Global universe declarations

7 files changed, 47 insertions, 48 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index b80741269..cb1d2f7c7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -126,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
-    Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
+    Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm);
     instance_hook k info global imps ?hook (ConstRef kn);
     id
 
@@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
           (ParameterEntry
             (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
         in
-          Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
+          Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars);
           instance_hook k pri global imps ?hook (ConstRef cst); id
       end
     else (
diff --git a/vernac/command.ml b/vernac/command.ml
index 01c7f149b..66d4fe984 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -95,7 +95,7 @@ let interp_definition pl bl poly red_option c ctypopt =
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
   let nb_args = Context.Rel.nhyps ctx in
-  let imps,pl,ce =
+  let imps,ce =
     match ctypopt with
       None ->
         let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -105,11 +105,10 @@ let interp_definition pl bl poly red_option c ctypopt =
 	let c = EConstr.Unsafe.to_constr c in
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let vars = Univops.universes_of_constr body in
-        let evd = Evd.restrict_universe_context !evdref vars in
-        let uctx = Evd.check_univ_decl ~poly evd decl in
-        let binders = Evd.universe_binders evd in
-        imps1@(Impargs.lift_implicits nb_args imps2), binders,
+        let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+        let () = evdref := Evd.restrict_universe_context !evdref vars in
+        let uctx = Evd.check_univ_decl ~poly !evdref decl in
+        imps1@(Impargs.lift_implicits nb_args imps2),
           definition_entry ~univs:uctx body
     | Some ctyp ->
         let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
@@ -131,23 +130,22 @@ let interp_definition pl bl poly red_option c ctypopt =
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
 	then warn_implicits_in_term ();
-        let vars = Univ.LSet.union (Univops.universes_of_constr body) 
-          (Univops.universes_of_constr typ) in
-        let ctx = Evd.restrict_universe_context !evdref vars in
-        let uctx = Evd.check_univ_decl ~poly ctx decl in
-        let binders = Evd.universe_binders evd in
-        imps1@(Impargs.lift_implicits nb_args impsty), binders,
-          definition_entry ~types:typ
-	    ~univs:uctx body
+        let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+        let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in
+        let vars = Univ.LSet.union bodyvars tyvars in
+        let () = evdref := Evd.restrict_universe_context !evdref vars in
+        let uctx = Evd.check_univ_decl ~poly !evdref decl in
+        imps1@(Impargs.lift_implicits nb_args impsty),
+          definition_entry ~types:typ ~univs:uctx body
   in
-  red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
+  (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps)
 
-let check_definition (ce, evd, _, _, imps) =
+let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
 let do_definition ident k univdecl bl red_option c ctypopt hook =
-  let (ce, evd, univdecl, pl', imps as def) =
+  let (ce, evd, univdecl, imps as def) =
     interp_definition univdecl bl (pi2 k) red_option c ctypopt
   in
     if Flags.is_program_mode () then
@@ -168,7 +166,7 @@ let do_definition ident k univdecl bl red_option c ctypopt hook =
       ignore(Obligations.add_definition
           ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(DeclareDef.declare_definition ident k ce pl' imps
+      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -224,7 +222,7 @@ match local with
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Universes.register_universe_binders gr pl in
+  let () = Declare.declare_univ_binders gr pl in
   let () = assumption_message ident in
   let () = if do_instance then Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
@@ -712,7 +710,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
 	      let ind = (mind,i) in
 	      let gr = IndRef ind in
 	      maybe_declare_manual_implicits false gr indimpls;
-	      Universes.register_universe_binders gr pl;
+              Declare.declare_univ_binders gr pl;
 	      List.iteri
 		(fun j impls ->
 		 maybe_declare_manual_implicits false
@@ -1268,7 +1266,7 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive local p fixkind fixl ntns =
+let do_program_recursive local poly fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info = 
     interp_recursive isfix fixl ntns 
@@ -1310,8 +1308,8 @@ let do_program_recursive local p fixkind fixl ntns =
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
-  | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
+  | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
+  | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
   in
   Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
 
diff --git a/vernac/command.mli b/vernac/command.mli
index 070f3e112..a1f916c78 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -28,7 +28,7 @@ val do_constraint : polymorphic ->
 val interp_definition :
   Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
-                        Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
+                        Univdecls.universe_decl * Impargs.manual_implicits
 
 val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 980db4109..dfac78c04 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps =
   let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Universes.register_universe_binders gr pl in
+  let () = Declare.declare_univ_binders gr pl in
   let () = definition_message ident in
   gr
 
@@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let () = definition_message ident in
     let gr = VarRef ident in
     let () = maybe_declare_manual_implicits false gr imps in
+    let () = Declare.declare_univ_binders gr pl in
     let () = if Proof_global.there_are_pending_proofs () then
 	       warn_definition_not_visible ident
     in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42631a15b..200c2260e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -177,7 +177,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
           (locality, ConstRef kn)
     in
     definition_message id;
-    Universes.register_universe_binders r (Option.default Universes.empty_binders pl);
+    Declare.declare_univ_binders r (UState.universe_binders uctx);
     call_hook (fun exn -> exn) hook l r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
@@ -286,17 +286,17 @@ let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
 let save_named ?export_seff proof =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
-  save ?export_seff id const cstrs pl do_guard persistence hook
+  let id,const,uctx,do_guard,persistence,hook = proof in
+  save ?export_seff id const uctx do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     user_err Pp.(str "This command can only be used for unnamed theorem.")
 
 let save_anonymous ?export_seff proof save_ident =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+  let id,const,uctx,do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save ?export_seff save_ident const cstrs pl do_guard persistence hook
+  save ?export_seff save_ident const uctx do_guard persistence hook
 
 (* Admitted *)
 
@@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () =
   | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
   in
   let () = assumption_message id in
-  Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl);
+  Declare.declare_univ_binders (ConstRef kn) pl;
   call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
@@ -330,8 +330,8 @@ let get_proof proof do_guard hook opacity =
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in
   make_terminator begin function
-  | Admitted (id,k,pe,(ctx,pl)) ->
-      admit (id,k,pe) pl (hook (Some ctx)) ();
+  | Admitted (id,k,pe,ctx) ->
+      admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
       Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff = match opaque with
@@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
         | Vernacexpr.Opaque      -> true, false
       in
       let proof = get_proof proof compute_guard
-	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
+        (hook (Some (proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
       | Some (_,id) -> save_anonymous ~export_seff proof id
@@ -417,7 +417,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
   | (id,(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
-        | None -> Evd.empty_evar_universe_context
+        | None -> UState.empty
         | Some ctx -> ctx
         in
         let other_thms_data =
@@ -426,9 +426,9 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ctx ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-            let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
             let body = Option.map norm body in
-            List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
+            let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
+            List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
@@ -496,7 +496,7 @@ let save_proof ?proof = function
             if const_entry_type = None then
               user_err Pp.(str "Admitted requires an explicit statement");
             let typ = Option.get const_entry_type in
-            let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in
+            let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
             Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
         | None ->
@@ -518,12 +518,9 @@ let save_proof ?proof = function
                   Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
               | _ -> None in
 	    let decl = Proof_global.get_universe_decl () in
-            let evd = Evd.from_ctx universes in
             let poly = pi2 k in
-            let ctx = Evd.check_univ_decl ~poly evd decl in
-            let binders = if poly then Some (UState.universe_binders universes) else None in
-            Admitted(id,k,(sec_vars, (typ, ctx), None),
-		     (universes, binders))
+            let ctx = UState.check_univ_decl ~poly universes decl in
+            Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1046d68f8..24d664951 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -833,7 +833,7 @@ let obligation_terminator name num guard hook auto pf =
     let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
     let ty = entry.Entries.const_entry_type in
     let (body, cstr), () = Future.force entry.Entries.const_entry_body in
-    let sigma = Evd.from_ctx (fst uctx) in
+    let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
     Inductiveops.control_only_guard (Global.env ()) body;
     (** Declare the obligation ourselves and drop the hook *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1d255b08e..1cdc538b5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -613,7 +613,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
     States.with_state_protection (fun () ->
       typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
-  match kind with
+  let gr = match kind with
   | Class def ->
      let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
      let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild
@@ -638,3 +638,6 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
+  in
+  Declare.declare_univ_binders gr pl;
+  gr