Merge PR #10419: [api] Refactor most of `Decl_kinds`

Reviewed-by: SkySkimmer
Ack-by: herbelin

8 files changed, 27 insertions, 29 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f773b2c39e..bf2b4c9122 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -992,7 +992,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
   let info = Lemmas.Info.make
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-      ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+      ~kind:(Decls.(IsProof Theorem)) () in
 
   let lemma = Lemmas.start_lemma
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3bab750534..cb7a509829 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -369,9 +369,9 @@ let generate_functional_principle (evd: Evd.evar_map ref)
         let ce = Declare.definition_entry ~univs value in
         ignore(
           Declare.declare_constant
-            name
-            (Declare.DefinitionEntry ce,
-             Decl_kinds.IsDefinition (Decl_kinds.Scheme))
+            ~name
+            ~kind:Decls.(IsDefinition Scheme)
+            (Declare.DefinitionEntry ce)
         );
         Declare.definition_message name;
         names := name :: !names
@@ -387,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 (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
+  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(IsProof Theorem)
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
@@ -637,8 +637,9 @@ let build_scheme fas =
     (fun (princ_id,_,_) def_entry ->
        ignore
          (Declare.declare_constant
-            princ_id
-            (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+            ~name:princ_id
+            ~kind:Decls.(IsProof Theorem)
+            (Declare.DefinitionEntry def_entry));
        Declare.definition_message princ_id
     )
     fas
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index bb4e745fe9..bcad6cedf1 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1506,7 +1506,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds ~cumulative:false ~poly:false ~private_ind:false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d305a58ccc..9a9e0b9692 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -419,7 +419,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
         ~name:fname
         ~poly:false
         ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-        ~kind:Decl_kinds.Definition pl
+        ~kind:Decls.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
          List.fold_left
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 56ed406e2f..58b0ead130 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,21 +123,19 @@ open DeclareDef
 
 let definition_message = Declare.definition_message
 
-let save id const ?hook uctx scope kind =
+let save name const ?hook uctx scope kind =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match scope with
     | Discharge ->
-        let k = Kindops.logical_kind_of_goal_kind kind in
-        let c = SectionLocalDef const in
-        let _ = declare_variable id (Lib.cwd(), c, k) in
-        VarRef id
+      let c = SectionLocalDef const in
+      let _ = declare_variable ~name ~kind (Lib.cwd(), c) in
+      VarRef name
     | Global local ->
-        let k = Kindops.logical_kind_of_goal_kind kind in
-        let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in
-        ConstRef kn
+      let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
+      ConstRef kn
   in
   DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
-  definition_message id
+  definition_message name
 
 let with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 45d332031f..a95b1242ac 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -48,7 +48,7 @@ val save
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> DeclareDef.locality
-  -> Decl_kinds.goal_object_kind
+  -> Decls.logical_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 86defb2f2f..549f6d42c9 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let (typ,_) = lemmas_types_infos.(i) in
          let info = Lemmas.Info.make
              ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-             ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+             ~kind:(Decls.(IsProof Theorem)) () in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
              ~poly:false
@@ -871,7 +871,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lem_id = mk_complete_id f_id in
          let info = Lemmas.Info.make
              ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-             ~kind:Decl_kinds.(Proof Theorem) () in
+             ~kind:Decls.(IsProof 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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d38e28c0e7..8d6b85f94d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -30,7 +30,6 @@ open Tacmach
 open Tactics
 open Nametab
 open Declare
-open Decl_kinds
 open Tacred
 open Goal
 open Glob_term
@@ -66,9 +65,9 @@ let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
   locate (make_qualid dp (Id.of_string s))
 
-let declare_fun f_id kind ?univs value =
+let declare_fun name kind ?univs value =
   let ce = definition_entry ?univs value (*FIXME *) in
-    ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+  ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
 
 let defined lemma =
   Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
@@ -196,7 +195,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
     let body = EConstr.Unsafe.to_constr body in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
+let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -1368,7 +1367,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma)
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(IsProof Lemma))
       () in
   let lemma = Lemmas.start_lemma
       ~name:na
@@ -1411,7 +1410,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
+    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
         ~sign:(Environ.named_context_val env)
@@ -1535,7 +1534,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref =
     let univs = Evd.univ_entry ~poly:false evd in
-    declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
+    declare_fun functional_id Decls.(IsDefinition Definition) ~univs res
   in
   (* Refresh the global universes, now including those of _F *)
   let evd = Evd.from_env (Global.env ()) in
@@ -1549,7 +1548,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
   (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook { DeclareDef.Hook.S.uctx ; _ } =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
-    let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
+    let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref in
     let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
     (*     message "start second proof"; *)
     let stop =