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

6 files changed, 51 insertions, 44 deletions

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