Allow declaring universe constraints at definition level.

Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof.  By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.

Declarations of universe binders and constraints also works for
monomorphic definitions.

4 files changed, 35 insertions, 29 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 193788558..23f96b5a3 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -239,7 +239,6 @@ let get_current_proof_name = Proof_global.get_current_proof_name
 let get_all_proof_names = Proof_global.get_all_proof_names
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
-type universe_binders = Proof_global.universe_binders
 
 let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
@@ -257,6 +256,5 @@ let set_used_variables l =
 let get_used_variables () =
   Proof_global.get_used_variables ()
 
-let get_universe_binders () =
-  Proof_global.get_universe_binders ()
-
+let get_universe_decl () =
+  Proof_global.get_universe_decl ()
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 745ee8f36..6e4ecd13b 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -23,7 +23,7 @@ open Decl_kinds
     proof of mutually dependent theorems) *)
 
 val start_proof :
-  Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+  Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -67,6 +67,7 @@ val current_proof_statement :
   unit -> Id.t * goal_kind * EConstr.types
 
 (** {6 ... } *)
+
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof or raises a [UserError] if no
     proof is focused or if there is no [n]th subgoal. [solve SelectAll
@@ -185,8 +186,8 @@ val get_used_variables : unit -> Context.Named.t option
 [@@ocaml.deprecated "use Proof_global.get_used_variables"]
 
 (** {6 Universe binders } *)
-val get_universe_binders : unit -> Proof_global.universe_binders option
-[@@ocaml.deprecated "use Proof_global.get_universe_binders"]
+val get_universe_decl : unit -> Univdecls.universe_decl
+[@@ocaml.deprecated "use Proof_global.get_universe_decl"]
 
 (** {6 ... } *)
 (** [get_current_proof_name ()] return the name of the current focused
@@ -202,7 +203,3 @@ val get_all_proof_names : unit -> Id.t list
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
 [@@ocaml.deprecated "use Proof_global.lemma_possible_guards"]
-
-type universe_binders = Proof_global.universe_binders
-[@@ocaml.deprecated "use Proof_global.universe_binders"]
-
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2ade797f6..e8266f5c8 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -69,7 +69,6 @@ let _ =
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
 type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
-type universe_binders = Id.t Loc.located list
 
 type proof_object = {
   id : Names.Id.t;
@@ -94,7 +93,7 @@ type pstate = {
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
-  universe_binders: universe_binders option;
+  universe_decl: Univdecls.universe_decl;
 }
 
 let make_terminator f = f
@@ -230,15 +229,22 @@ let activate_proof_mode mode =
 let disactivate_current_proof_mode () =
   CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
 
-(** [start_proof sigma id str goals terminator] starts a proof of name
+let default_universe_decl =
+  let open Misctypes in
+  { univdecl_instance = [];
+    univdecl_extensible_instance = true;
+    univdecl_constraints = Univ.Constraint.empty;
+    univdecl_extensible_constraints = true }
+
+(** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
-    constraints). *)
-let start_proof sigma id ?pl str goals terminator =
+    constraints), and with universe bindings pl. *)
+let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -247,10 +253,10 @@ let start_proof sigma id ?pl str goals terminator =
     section_vars = None;
     strength = str;
     mode = find_proof_mode "No";
-    universe_binders = pl } in
+    universe_decl = pl } in
   push initial_state pstates
 
-let start_dependent_proof id ?pl str goals terminator =
+let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -259,11 +265,11 @@ let start_dependent_proof id ?pl str goals terminator =
     section_vars = None;
     strength = str;
     mode = find_proof_mode "No";
-    universe_binders = pl } in
+    universe_decl = pl } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
-let get_universe_binders () = (cur_pstate ()).universe_binders
+let get_universe_decl () = (cur_pstate ()).universe_decl
 
 let proof_using_auto_clear = ref false
 let _ = Goptions.declare_bool_option
@@ -319,7 +325,7 @@ type closed_proof_output = (Term.constr * Safe_typing.private_constants) list *
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
-  let { pid; section_vars; strength; proof; terminator; universe_binders } =
+  let { pid; section_vars; strength; proof; terminator; universe_decl } =
     cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
@@ -393,8 +399,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
         })
 		fpl initial_goals in
   let binders =
-    Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
-	       universe_binders
+    if not poly || (List.is_empty universe_decl.Misctypes.univdecl_instance &&
+                    universe_decl.Misctypes.univdecl_extensible_instance) then None
+    else
+      Some (fst (Evd.check_univ_decl (Evd.from_ctx universes) universe_decl))
   in
   { id = pid; entries = entries; persistence = strength;
     universes = (universes, binders) },
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 52f5f7404..8c0f6ad85 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -34,7 +34,7 @@ val compact_the_proof : unit -> unit
     values. *)
 type lemma_possible_guards = int list list
 type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
-type universe_binders = Names.Id.t Loc.located list
+
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
@@ -54,21 +54,23 @@ type closed_proof = proof_object * proof_terminator
 val make_terminator : (proof_ending -> unit) -> proof_terminator
 val apply_terminator : proof_terminator -> proof_ending -> unit
 
-(** [start_proof id str goals terminator] starts a proof of name [id]
+(** [start_proof id str pl goals terminator] starts a proof of name [id]
     with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
-    end of the proof to close the proof. *)
+    end of the proof to close the proof. The proof is started in the
+    evar map [sigma] (which can typically contain universe
+    constraints), and with universe bindings pl. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
+  Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind ->
+  Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
   Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
@@ -119,7 +121,8 @@ val set_used_variables :
   Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list
 val get_used_variables : unit -> Context.Named.t option
 
-val get_universe_binders : unit -> universe_binders option
+(** Get the universe declaration associated to the current proof. *)
+val get_universe_decl : unit -> Univdecls.universe_decl
 
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *