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

19 files changed, 103 insertions, 79 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 0e2ef95739..4b20016ab2 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -67,7 +67,7 @@ type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = locality * polymorphic * goal_object_kind
+type goal_kind = locality * goal_object_kind
 
 (** Kinds used in library *)
 
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 22e20e2c52..8c2cf3c553 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -19,7 +19,8 @@ let start_deriving f suchthat name : Lemmas.t =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in
+  let poly = false in
+  let kind = Decl_kinds.(Global ImportDefaultBehavior,DefinitionBody Definition) in
 
   (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
@@ -40,7 +41,7 @@ let start_deriving f suchthat name : Lemmas.t =
   in
 
   let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in
-  let lemma = Lemmas.start_dependent_lemma ~name ~kind ~info goals in
+  let lemma = Lemmas.start_dependent_lemma ~name ~poly ~kind ~info goals in
   Lemmas.pf_map (Proof_global.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
   end) lemma
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
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 49265802ae..d87b7a1770 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1994,7 +1994,8 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
-  let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic,
+  let poly = atts.polymorphic in
+  let kind = Decl_kinds.(Global ImportDefaultBehavior),
              Decl_kinds.DefinitionBody Decl_kinds.Instance
   in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -2010,7 +2011,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let info = Lemmas.Info.make ~hook () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~name:instance_id ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
        fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
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
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e4fa5e84b4..68a2a0afe0 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -103,8 +103,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
      question, how does abstract behave when discharge is local for example?
   *)
   let goal_kind, suffix = if opaque
-    then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof"
-    else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in
+    then (Global ImportDefaultBehavior,Proof Theorem), "_subproof"
+    else (Global ImportDefaultBehavior,DefinitionBody Definition), "_subterm" in
   let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
@@ -141,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac
+    try Pfedit.build_constant_by_tactic ~poly ~goal_kind id ectx secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 37af8e1f55..bb5ebd7148 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -373,10 +373,10 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
      the refinement manually.*)
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
-  let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
+  let kind = Decl_kinds.Global ImportDefaultBehavior, Decl_kinds.DefinitionBody Decl_kinds.Instance in
   let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in
   let info = Lemmas.Info.make ~hook () in
-  let lemma = Lemmas.start_lemma ~name:id ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in
+  let lemma = Lemmas.start_lemma ~name:id ~poly ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     if not (Option.is_empty term) then
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 31c2053148..6d9aa746b9 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -269,7 +269,7 @@ let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,f
     Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in
   let evd = Evd.from_ctx ctx in
   let lemma =
-    Lemmas.start_lemma_with_initialization ~kind:(local,poly,DefinitionBody fix_kind) ~udecl
+    Lemmas.start_lemma_with_initialization ~poly ~kind:(local,DefinitionBody fix_kind) ~udecl
       evd (Some(cofix,indexes,init_tac)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index c3dfdd1c0f..d323493c11 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -246,7 +246,7 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
-let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i
+let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq i
     { Recthm.name; typ; impargs } =
   let t_i = norm typ in
   let k = IsAssumption Conjectural in
@@ -261,7 +261,7 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i
               Univ.ContextSet.of_context univs
             | Monomorphic_entry univs -> univs
           in
-          let c = SectionLocalAssum ((t_i, univs),p,impl) in
+          let c = SectionLocalAssum ((t_i, univs),poly,impl) in
           let _ = declare_variable name (Lib.cwd(),c,k) in
           (VarRef name,impargs)
       | Global local ->
@@ -338,19 +338,19 @@ module Stack = struct
 end
 
 (* Starting a goal *)
-let start_lemma ~name ~kind
+let start_lemma ~name ~poly ~kind
     ?(udecl=UState.default_univ_decl)
     ?(sign=initialize_named_context_for_proof())
     ?(info=Info.make ())
     sigma c =
   let goals = [ Global.env_of_context sign , c ] in
-  let proof = Proof_global.start_proof sigma name udecl kind goals in
+  let proof = Proof_global.start_proof sigma name udecl ~poly kind goals in
   { proof ; info }
 
-let start_dependent_lemma ~name ~kind
+let start_dependent_lemma ~name ~poly ~kind
     ?(udecl=UState.default_univ_decl)
     ?(info=Info.make ()) telescope =
-  let proof = Proof_global.start_dependent_proof name udecl kind telescope in
+  let proof = Proof_global.start_dependent_proof name udecl ~poly kind telescope in
   { proof; info }
 
 let rec_tac_initializer finite guard thms snl =
@@ -367,7 +367,7 @@ let rec_tac_initializer finite guard thms snl =
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_lemma_with_initialization ?hook ~kind ~udecl sigma recguard thms snl =
+let start_lemma_with_initialization ?hook ~poly ~kind ~udecl sigma recguard thms snl =
   let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
   let init_tac, compute_guard = match recguard with
   | Some (finite,guard,init_tac) ->
@@ -392,13 +392,13 @@ let start_lemma_with_initialization ?hook ~kind ~udecl sigma recguard thms snl =
            ; other_thms
            ; proof_ending = CEphemeron.create Proof_ending.Regular
            } in
-    let lemma = start_lemma ~name ~kind ~udecl ~info sigma typ in
+    let lemma = start_lemma ~name ~poly ~kind ~udecl ~info sigma typ in
     pf_map (Proof_global.map_proof (fun p ->
         match init_tac with
         | None -> p
         | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma
 
-let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms =
+let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
@@ -409,7 +409,7 @@ let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms =
     let hook = inference_hook in
     let evd = solve_remaining_evars ?hook flags env evd in
     let ids = List.map RelDecl.get_name ctx in
-    check_name_freshness (pi1 kind) id;
+    check_name_freshness (fst kind) id;
     (* XXX: The nf_evar is critical !! *)
     evd, (id.CAst.v,
           (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
@@ -424,14 +424,14 @@ let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms =
   let () =
     let open UState in
     if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
-       ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd udecl)
+       ignore (Evd.check_univ_decl ~poly evd udecl)
   in
   let evd =
-    if pi2 kind then evd
+    if poly then evd
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  start_lemma_with_initialization ?hook ~kind evd ~udecl recguard thms snl
+  start_lemma_with_initialization ?hook ~poly ~kind evd ~udecl recguard thms snl
 
 (************************************************************************)
 (* Admitting a lemma-like constant                                      *)
@@ -449,19 +449,19 @@ let warn_let_as_axiom =
 
 (* This declares implicits and calls the hooks for all the theorems,
    including the main one *)
-let process_recthms ?fix_exn ?hook env sigma ctx decl strength ref imps other_thms =
+let process_recthms ?fix_exn ?hook env sigma ctx decl ~poly strength ref imps other_thms =
   let other_thms_data =
     if List.is_empty other_thms then [] else
       (* there are several theorems defined mutually *)
       let body,opaq = retrieve_first_recthm ctx ref in
       let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
       let body = Option.map EConstr.of_constr body in
-      let uctx = UState.check_univ_decl ~poly:(pi2 strength) ctx decl in
-      List.map_i (save_remaining_recthms env sigma strength norm uctx body opaq) 1 other_thms in
+      let uctx = UState.check_univ_decl ~poly ctx decl in
+      List.map_i (save_remaining_recthms env sigma ~poly strength norm uctx body opaq) 1 other_thms in
   let thms_data = (ref,imps)::other_thms_data in
   List.iter (fun (ref,imps) ->
       maybe_declare_manual_implicits false ref imps;
-      DeclareDef.Hook.call ?fix_exn ?hook ctx [] (pi1 strength) ref) thms_data
+      DeclareDef.Hook.call ?fix_exn ?hook ctx [] (fst strength) ref) thms_data
 
 let get_keep_admitted_vars =
   Goptions.declare_bool_option_and_ref
@@ -470,7 +470,7 @@ let get_keep_admitted_vars =
     ~key:["Keep"; "Admitted"; "Variables"]
     ~value:true
 
-let finish_admitted env sigma id (scope,poly,kind) pe ctx hook udecl impargs other_thms =
+let finish_admitted env sigma id ~poly (scope,kind) pe ctx hook udecl impargs other_thms =
   let local = match scope with
   | Global local -> local
   | Discharge -> warn_let_as_axiom id; ImportNeedQualified
@@ -479,7 +479,7 @@ let finish_admitted env sigma id (scope,poly,kind) pe ctx hook udecl impargs oth
   let () = assumption_message id in
   Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx);
   (* This takes care of the implicits and hook for the current constant*)
-  process_recthms ?fix_exn:None ?hook env sigma ctx udecl (Global local,poly,kind) (ConstRef kn) impargs other_thms;
+  process_recthms ?fix_exn:None ?hook env sigma ctx udecl ~poly (Global local,kind) (ConstRef kn) impargs other_thms;
   Feedback.feedback Feedback.AddedAxiom
 
 let save_lemma_admitted ?proof ~(lemma : t) =
@@ -489,14 +489,17 @@ let save_lemma_admitted ?proof ~(lemma : t) =
     | Some ({ id; entries; persistence = k; universes; udecl }, { Info.hook; impargs; other_thms; _} ) ->
       if List.length entries <> 1 then
         user_err Pp.(str "Admitted does not support multiple statements");
-      let { proof_entry_secctx; proof_entry_type } = List.hd entries in
+      let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
       if proof_entry_type = None then
         user_err Pp.(str "Admitted requires an explicit statement");
+      let poly = match proof_entry_universes with
+        | Entries.Monomorphic_entry _ -> false
+        | Entries.Polymorphic_entry (_, _) -> true in
       let typ = Option.get proof_entry_type in
-      let ctx = UState.univ_entry ~poly:(pi2 k) universes in
+      let ctx = UState.univ_entry ~poly universes in
       let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
       let sigma = Evd.from_env env in
-      finish_admitted env sigma id k (sec_vars, (typ, ctx), None) universes hook udecl impargs other_thms
+      finish_admitted env sigma id k (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms
     | None ->
       let pftree = Proof_global.get_proof lemma.proof in
       let gk = Proof_global.get_persistence lemma.proof in
@@ -526,7 +529,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
       let { Info.hook; impargs; other_thms } = lemma.info in
       let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
       let ctx = UState.check_univ_decl ~poly universes udecl in
-      finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook udecl impargs other_thms
+      finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -536,7 +539,7 @@ let finish_proved env sigma opaque idopt po info =
   let open Proof_global in
   let { Info.hook; compute_guard; impargs; other_thms } = info in
   match po with
-  | { id; entries=[const]; persistence=locality,poly,kind; universes; udecl } ->
+  | { id; entries=[const]; persistence=locality,kind; universes; udecl; poly } ->
     let is_opaque = match opaque with
       | Transparent -> false
       | Opaque      -> true
@@ -570,7 +573,7 @@ let finish_proved env sigma opaque idopt po info =
       in
       definition_message id;
       (* This takes care of the implicits and hook for the current constant*)
-      process_recthms ~fix_exn ?hook env sigma universes udecl (locality,poly,kind) r impargs other_thms
+      process_recthms ~fix_exn ?hook env sigma universes udecl ~poly (locality,kind) r impargs other_thms
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
       iraise (fix_exn e)
@@ -627,7 +630,7 @@ let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 =
 
   let open Decl_kinds in
   let obls = ref 1 in
-  let kind = match pi3 proof_obj.Proof_global.persistence with
+  let kind = match snd proof_obj.Proof_global.persistence with
     | DefinitionBody d -> IsDefinition d
     | Proof p -> IsProof p
   in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 28b9c38072..1a8b1f2f30 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -93,6 +93,7 @@ end
 (** Starts the proof of a constant *)
 val start_lemma
   :  name:Id.t
+  -> poly:bool
   -> kind:goal_kind
   -> ?udecl:UState.universe_decl
   -> ?sign:Environ.named_context_val
@@ -103,6 +104,7 @@ val start_lemma
 
 val start_dependent_lemma
   :  name:Id.t
+  -> poly:bool
   -> kind:goal_kind
   -> ?udecl:UState.universe_decl
   -> ?info:Info.t
@@ -114,6 +116,7 @@ type lemma_possible_guards = int list list
 (** Pretty much internal, only used in ComFixpoint *)
 val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
+  -> poly:bool
   -> kind:goal_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
@@ -127,6 +130,7 @@ val default_thm_id : Names.Id.t
 (** Main [Lemma foo args : type.] command *)
 val start_lemma_com
   :  program_mode:bool
+  -> poly:bool
   -> kind:goal_kind
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:DeclareDef.Hook.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 4e4f80fd71..b2c5520c0b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -388,16 +388,14 @@ let deps_remaining obls deps =
     deps []
 
 
-let goal_kind poly =
-  Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition)
+let goal_kind = Decl_kinds.(Global ImportNeedQualified, DefinitionBody Definition)
+let goal_proof_kind = Decl_kinds.(Global ImportNeedQualified, Proof Lemma)
 
-let goal_proof_kind poly =
-  Decl_kinds.(Global ImportNeedQualified, poly, Proof Lemma)
-
-let kind_of_obligation poly o =
+let kind_of_obligation o =
   match o with
-  | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
-  | _ -> goal_proof_kind poly
+  | Evar_kinds.Define false
+  | Evar_kinds.Expand -> goal_kind
+  | _ -> goal_proof_kind
 
 let rec string_of_list sep f = function
     [] -> ""
@@ -415,7 +413,7 @@ let solve_by_tac ?loc name evi t poly ctx =
   try
     let (entry,_,ctx') =
       Pfedit.build_constant_by_tactic
-        id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in
+        id ~poly ~goal_kind ctx evi.evar_hyps evi.evar_concl t in
     let env = Global.env () in
     let (body, eff) = Future.force entry.Proof_global.proof_entry_body in
     let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
@@ -486,14 +484,15 @@ let rec solve_obligation prg num tac =
         ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
   in
   let obl = subst_deps_obl obls obl in
-  let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in
+  let kind = kind_of_obligation (snd obl.obl_status) in
   let evd = Evd.from_ctx prg.prg_ctx in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n oblset tac = auto_solve_obligations n ~oblset tac in
   let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in
   let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in
   let info = Lemmas.Info.make ~hook ~proof_ending () in
-  let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~kind ~info evd (EConstr.of_constr obl.obl_type) in
+  let poly = pi2 prg.prg_kind in
+  let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~kind ~info evd (EConstr.of_constr obl.obl_type) in
   let lemma = fst @@ Lemmas.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
   lemma
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index da8808ccaa..d1377fecc5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -560,7 +560,7 @@ let () =
 (***********)
 (* Gallina *)
 
-let start_proof_and_print ~program_mode ?hook k l =
+let start_proof_and_print ~program_mode ~poly ?hook k l =
   let inference_hook =
     if program_mode then
       let hook env sigma ev =
@@ -582,7 +582,7 @@ let start_proof_and_print ~program_mode ?hook k l =
       in Some hook
     else None
   in
-  start_lemma_com ~program_mode ?inference_hook ?hook ~kind:k l
+  start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~kind:k l
 
 let vernac_definition_hook p = function
 | Coercion ->
@@ -614,8 +614,9 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
   let program_mode = atts.program in
+  let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
-  start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)]
+  start_proof_and_print ~program_mode ~poly (local, DefinitionBody kind) ?hook [(name, pl), (bl, t)]
 
 let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
@@ -638,7 +639,7 @@ let vernac_start_proof ~atts kind l =
   let local = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
+  start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic (local, Proof kind) l
 
 let vernac_end_proof ?stack ?proof = let open Vernacexpr in function
   | Admitted ->