[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.

4 files changed, 25 insertions, 16 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)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index d01704926a..51cb3ca0ee 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -58,14 +58,18 @@ val use_unification_heuristics : unit -> bool
     [tac]. The return boolean, if [false] indicates the use of an unsafe
     tactic. *)
 
-val build_constant_by_tactic :
-  Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
-  EConstr.types -> unit Proofview.tactic -> 
-  Evd.side_effects Proof_global.proof_entry * bool *
-    UState.t
+val build_constant_by_tactic
+  :  Id.t
+  -> UState.t
+  -> named_context_val
+  -> poly:bool
+  -> ?goal_kind:goal_kind
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> Evd.side_effects Proof_global.proof_entry * bool * UState.t
 
 val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
-  EConstr.types -> unit Proofview.tactic -> 
+  EConstr.types -> unit Proofview.tactic ->
   constr * bool * UState.t
 
 val refine_by_tactic
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2f7e5d618a..22f818edbb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -39,6 +39,7 @@ type 'a proof_entry = {
 type proof_object =
   { id : Names.Id.t
   ; entries : Evd.side_effects proof_entry list
+  ; poly : bool
   ; persistence : Decl_kinds.goal_kind
   ; universes: UState.t
   ; udecl : UState.universe_decl
@@ -69,7 +70,8 @@ let map_fold_proof_endline f ps =
     | None -> Proofview.tclUNIT ()
     | Some tac ->
       let open Geninterp in
-      let ist = { lfun = Id.Map.empty; poly = pi2 ps.strength; extra = TacStore.empty } in
+      let {Proof.poly} = Proof.data ps.proof in
+      let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
       let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
       let tac = Geninterp.interp tag ist tac in
       Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
@@ -92,16 +94,16 @@ let set_endline_tactic tac ps =
     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. *)
-let start_proof sigma name udecl kind goals =
-  { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
+let start_proof sigma name udecl ~poly kind goals =
+  { proof = Proof.start ~name ~poly sigma goals
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
   ; strength = kind
   }
 
-let start_dependent_proof name udecl kind goals =
-  { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
+let start_dependent_proof name udecl ~poly kind goals =
+  { proof = Proof.dependent_start ~name ~poly goals
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
@@ -254,7 +256,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
       proof_entry_universes = univs; }
   in
   let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
-  { id = name; entries = entries; persistence = strength; universes; udecl }
+  { id = name; entries = entries; poly; persistence = strength; universes; udecl }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 3baa58084d..5bfed948ba 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,6 +46,7 @@ type 'a proof_entry = {
 type proof_object =
   { id : Names.Id.t
   ; entries : Evd.side_effects proof_entry list
+  ; poly : bool
   ; persistence : Decl_kinds.goal_kind
   ; universes: UState.t
   ; udecl : UState.universe_decl
@@ -65,6 +66,7 @@ val start_proof
   :  Evd.evar_map
   -> Names.Id.t
   -> UState.universe_decl
+  -> poly:bool
   -> Decl_kinds.goal_kind
   -> (Environ.env * EConstr.types) list
   -> t
@@ -74,6 +76,7 @@ val start_proof
 val start_dependent_proof
   :  Names.Id.t
   -> UState.universe_decl
+  -> poly:bool
   -> Decl_kinds.goal_kind
   -> Proofview.telescope
   -> t