[lemmas] [proof] Split proof kinds into per-layer components.

We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:

- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
  pushed upwards]

We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.

More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.

7 files changed, 39 insertions, 29 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c37e6f7402..0d3c7b365f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -990,13 +990,17 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       ]
   in
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
+  let info = Lemmas.Info.make
+      ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+      ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+
   let lemma = Lemmas.start_lemma
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
       ~name:(mk_equation_id f_id)
       ~poly:false
-      ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem))
+      ~info
       evd
       lemma_type
   in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1b447bd26a..65b114fc03 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -311,7 +311,6 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
     Lemmas.start_lemma
       ~name:new_princ_name
       ~poly:false
-      ~kind:(Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem))
       !evd
       (EConstr.of_constr new_principle_type)
   in
@@ -325,10 +324,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    end; *)
 
   let open Proof_global in
-  let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { id; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
   match entries with
   | [entry] ->
-    (id,(entry,persistence)), hook
+    id, entry, hook
   | _ ->
     CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
@@ -380,7 +379,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       register_with_sort InProp;
       register_with_sort InSet
   in
-  let ((id,(entry,g_kind)),hook) =
+  let id,entry,hook =
     build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
@@ -388,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx g_kind
+  save new_princ_name entry ~hook uctx Decl_kinds.(Global ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
@@ -519,7 +518,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro
         s::l_schemes -> s,l_schemes
       | _ -> anomaly (Pp.str "")
   in
-  let ((_,(const,_)),_) =
+  let _,const,_ =
     try
       build_functional_principle evd false
         first_type
@@ -577,10 +576,10 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro
 
              )
              ta;
-           (* If we reach this point, the two principle are not mutually recursive
-              We fall back to the previous method
-           *)
-             let ((_,(const,_)),_) =
+             (* If we reach this point, the two principle are not mutually recursive
+                We fall back to the previous method
+                *)
+             let _,const,_ =
                build_functional_principle
                  evd
                  false
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0ecfbacb09..b07a92658b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -416,8 +416,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
       ComDefinition.do_definition
         ~program_mode:false
-        fname
-        Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl
+        ~name:fname
+        ~poly:false
+        ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+        ~kind:Decl_kinds.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
          List.fold_left
@@ -434,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl;
+       ComFixpoint.do_fixpoint ~scope:(Global ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a5a07934ac..8745853180 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/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1d096fa488..602f7af57a 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,8 @@ val save
   -> Evd.side_effects Proof_global.proof_entry
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
-  -> Decl_kinds.goal_kind
+  -> Decl_kinds.locality
+  -> Decl_kinds.goal_object_kind
   -> unit
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e5b0a5d032..1ab64ac1b2 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -803,10 +803,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          i*)
          let lem_id = mk_correct_id f_id in
          let (typ,_) = lemmas_types_infos.(i) in
+         let info = Lemmas.Info.make
+             ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+             ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
              ~poly:false
-             ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem)
+             ~info
              !evd
              typ in
          let lemma = fst @@ Lemmas.by
@@ -866,13 +869,14 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
              Ensures by: obvious
            i*)
          let lem_id = mk_complete_id f_id in
-         let lemma = Lemmas.start_lemma ~name:lem_id
-             ~poly:false
-             ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma
-             (fst lemmas_types_infos.(i)) in
+         let info = Lemmas.Info.make
+             ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+             ~kind:Decl_kinds.(Proof Theorem) () in
+         let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
+             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
+                            (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
+                                                     (proving_tac i))) lemma) in
          let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
          let finfo = find_Function_infos (fst f_as_constant) in
          let _,lem_cst_constr = Evd.fresh_global
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 187d907dc5..6663fa5c60 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1367,11 +1367,12 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     in
     Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
   in
-  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
+  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
+      ~scope:Decl_kinds.(Global ImportDefaultBehavior) ~kind:Decl_kinds.(Proof Lemma)
+      () in
   let lemma = Lemmas.start_lemma
       ~name:na
-      ~poly:false (* FIXME *)
-      ~kind:Decl_kinds.(Global ImportDefaultBehavior, Proof Lemma) ~info
+      ~poly:false (* FIXME *) ~info
       sigma gls_type in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
@@ -1410,10 +1411,9 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let info = Lemmas.Info.make ~hook () in
+    let info = Lemmas.Info.make ~hook ~scope:(Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
-        ~kind:(Global ImportDefaultBehavior, Proof Lemma)
         ~sign:(Environ.named_context_val env)
         ~info
         ctx
@@ -1462,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 ~poly:false ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign evd
+    let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref