Stylistic improvements in intf/decl_kinds.mli.

We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.

The previously common idom:

if pi2 kind (* polymorphic *) then ... else ...

becomes:

if kind.polymorphic then ... else ...

To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".

3 files changed, 9 insertions, 6 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 86c2b7a57..d55d6ce6b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -147,7 +147,10 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
+let default_goal_kind =
+  { locality = Global; polymorphic = false; object_kind = Proof Theorem }
+
+let build_constant_by_tactic id ctx sign ?(goal_kind = default_goal_kind) typ tac =
   let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   start_proof id goal_kind evd sign typ terminator;
@@ -161,10 +164,10 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     delete_current_proof ();
     iraise reraise
 
-let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
+let build_by_tactic ?(side_eff=true) env ctx ?(polymorphic=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let gk = Global, poly, Proof Theorem in
+  let gk = { locality = Global; polymorphic; object_kind = Proof Theorem } in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
   let ce =
     if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f2f4b11ed..aa01969b7 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -169,7 +169,7 @@ val build_constant_by_tactic :
   types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
 
-val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
+val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?polymorphic:polymorphic ->
   types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2956d623f..911d4ffbc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -320,7 +320,7 @@ let constrain_variables init uctx =
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator; universe_binders } =
     cur_pstate () in
-  let poly = pi2 strength (* Polymorphic *) in
+  let poly = strength.Decl_kinds.polymorphic in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
@@ -398,7 +398,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 let return_proof ?(allow_partial=false) () =
- let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
+ let { pid; proof; strength = { Decl_kinds.polymorphic }} = cur_pstate () in
  if allow_partial then begin
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in