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

5 files changed, 17 insertions, 11 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9c593a55d8..c37e6f7402 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -995,8 +995,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       Ensures by: obvious
       i*)
       ~name:(mk_equation_id f_id)
-      ~kind:Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
-
+      ~poly:false
+      ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem))
       evd
       lemma_type
   in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1154198d43..1b447bd26a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -308,8 +308,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   evd := sigma;
   let hook = DeclareDef.Hook.make (hook new_principle_type) in
   let lemma =
-    Lemmas.start_lemma ~name:new_princ_name
-      ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+    Lemmas.start_lemma
+      ~name:new_princ_name
+      ~poly:false
+      ~kind:(Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem))
       !evd
       (EConstr.of_constr new_principle_type)
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 17c79e0e6c..a5a07934ac 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,7 +123,7 @@ open Declare
 
 let definition_message = Declare.definition_message
 
-let save id const ?hook uctx (locality,_,kind) =
+let save id const ?hook uctx (locality,kind) =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match locality with
     | Discharge ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 48b5e56635..e5b0a5d032 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let (typ,_) = lemmas_types_infos.(i) in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
-             ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+             ~poly:false
+             ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem)
              !evd
              typ in
          let lemma = fst @@ Lemmas.by
@@ -866,8 +867,9 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
            i*)
          let lem_id = mk_complete_id f_id in
          let lemma = Lemmas.start_lemma ~name:lem_id
-           ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
-         (fst lemmas_types_infos.(i)) in
+             ~poly:false
+             ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma
+             (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
            (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
               (proving_tac i))) lemma) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c97b39ff79..187d907dc5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1370,7 +1370,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
   let lemma = Lemmas.start_lemma
       ~name:na
-      ~kind:Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~info
+      ~poly:false (* FIXME *)
+      ~kind:Decl_kinds.(Global ImportDefaultBehavior, Proof Lemma) ~info
       sigma gls_type in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
@@ -1411,7 +1412,8 @@ let com_terminate
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
     let info = Lemmas.Info.make ~hook () in
     let lemma = Lemmas.start_lemma ~name:thm_name
-        ~kind:(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
+        ~poly:false (*FIXME*)
+        ~kind:(Global ImportDefaultBehavior, Proof Lemma)
         ~sign:(Environ.named_context_val env)
         ~info
         ctx
@@ -1460,7 +1462,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let evd = Evd.from_ctx uctx in
     let f_constr = constr_of_monomorphic_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    let lemma = Lemmas.start_lemma ~name:eq_name ~kind:(Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+    let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref