[proof] Remove duplicated universe polymorphic from decl_kinds

This information is already present on `Proof.t`, so we extract it
form there.

Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.

1 files changed, 4 insertions, 4 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d00f2c4803..64d21be7e8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -116,10 +116,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 ImportDefaultBehavior, false, Proof Theorem) typ tac =
+let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaultBehavior, Proof Theorem) typ tac =
   let evd = Evd.from_ctx ctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof evd id UState.default_univ_decl goal_kind goals in
+  let pf = Proof_global.start_proof evd id ~poly UState.default_univ_decl goal_kind goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
@@ -137,9 +137,9 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehav
 let build_by_tactic ?(side_eff=true) env sigma ?(poly=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 ImportDefaultBehavior, poly, Proof Theorem in
+  let gk = Global ImportDefaultBehavior, Proof Theorem in
   let ce, status, univs =
-    build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
+    build_constant_by_tactic id sigma sign ~poly ~goal_kind:gk typ tac in
   let body, eff = Future.force ce.Proof_global.proof_entry_body in
   let (cb, ctx) =
     if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)