[decls] Remove goal_object_kind type.

We can use logical kind for the same purpose, which is mainly
dumpglob, so `goal_object_kind` was never matched against, making this
transformation safe.

16 files changed, 21 insertions, 45 deletions

diff --git a/interp/decls.ml b/interp/decls.ml
index 52685e0666..b802dbe9c3 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -48,13 +48,8 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context
    Logical      |  Hypothesis | Axiom
 
 *)
-(** Kinds used in proofs *)
 
-type goal_object_kind =
-  | DefinitionBody of definition_object_kind
-  | Proof of theorem_kind
-
-(** Kinds used in library *)
+(** Kinds *)
 
 type logical_kind =
   | IsPrimitive
@@ -62,10 +57,6 @@ type logical_kind =
   | IsDefinition of definition_object_kind
   | IsProof of theorem_kind
 
-let logical_kind_of_goal_kind = function
-  | DefinitionBody d -> IsDefinition d
-  | Proof s -> IsProof s
-
 (** Data associated to section variables and local definitions *)
 
 type variable_data =
diff --git a/interp/decls.mli b/interp/decls.mli
index ce29197891..05e4be0de6 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -45,11 +45,6 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context
    Logical      |  Hypothesis | Axiom
 
 *)
-(** Kinds used in proofs *)
-
-type goal_object_kind =
-  | DefinitionBody of definition_object_kind
-  | Proof of theorem_kind
 
 (** Kinds used in library *)
 
@@ -59,9 +54,6 @@ type logical_kind =
   | IsDefinition of definition_object_kind
   | IsProof of theorem_kind
 
-(** Operations *)
-val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
-
 (** This module manages non-kernel informations about declarations. It
     is either non-logical informations or logical informations that
     have no place to be (yet) in the kernel *)
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 780cf4af21..ead78f70a1 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -20,7 +20,7 @@ let start_deriving f suchthat name : Lemmas.t =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let poly = false in
-  let kind = Decls.(DefinitionBody Definition) in
+  let kind = Decls.(IsDefinition Definition) in
 
   (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 6a5307d8f5..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:(Decls.(Proof 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 41db9796b9..cb7a509829 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -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) Decls.(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)
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 17a96d0641..58b0ead130 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -127,12 +127,10 @@ 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 kind = Decls.logical_kind_of_goal_kind kind in
       let c = SectionLocalDef const in
       let _ = declare_variable ~name ~kind (Lib.cwd(), c) in
       VarRef name
     | Global local ->
-      let kind = Decls.logical_kind_of_goal_kind kind in
       let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
       ConstRef kn
   in
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1758efe584..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
-  -> Decls.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 153b27c855..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:(Decls.(Proof 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:Decls.(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 a05feed1d1..8d6b85f94d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1367,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:(Decls.(Proof Lemma))
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(IsProof Lemma))
       () in
   let lemma = Lemmas.start_lemma
       ~name:na
@@ -1410,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:Decls.(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)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index bef0dcc189..13844c2707 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1994,7 +1994,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
   let poly = atts.polymorphic in
-  let kind = Decls.(DefinitionBody Instance) in
+  let kind = Decls.(IsDefinition Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
   let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
     | Globnames.ConstRef cst ->
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 99a755e222..24f4f7fe70 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -372,7 +372,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
-  let kind = Decls.(DefinitionBody Instance) in
+  let kind = Decls.(IsDefinition Instance) in
   let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in
   let info = Lemmas.Info.make ~hook ~scope ~kind () in
   let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index cc2f7d9f70..3f13d772ab 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -268,7 +268,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
     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 ~poly ~scope ~kind:(Decls.DefinitionBody fix_kind) ~udecl
+    Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition 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 226697a29a..d0e2e0f935 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -72,11 +72,11 @@ module Info = struct
     (* This could be improved and the CEphemeron removed *)
     ; other_thms : Recthm.t list
     ; scope : DeclareDef.locality
-    ; kind : Decls.goal_object_kind
+    ; kind : Decls.logical_kind
     }
 
   let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior)
-      ?(kind=Decls.(Proof Lemma)) () =
+      ?(kind=Decls.(IsProof Lemma)) () =
     { hook
     ; compute_guard = []
     ; impargs = []
@@ -494,7 +494,6 @@ let finish_proved env sigma idopt po info =
     let fix_exn = Future.fix_exn_of const.proof_entry_body in
     let () = try
       let const = adjust_guardness_conditions const compute_guard in
-      let kind = Decls.logical_kind_of_goal_kind kind in
       let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
       let open DeclareDef in
       let r = match scope with
@@ -571,10 +570,6 @@ let finish_derived ~f ~name ~idopt ~entries =
 let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
 
   let obls = ref 1 in
-  let kind = let open Decls in match kind with
-    | DefinitionBody d -> IsDefinition d
-    | Proof p -> IsProof p
-  in
   let sigma, recobls =
     CList.fold_left2_map (fun sigma (wit, (evar_env, ev, evi, local_context, type_)) entry ->
         let id =
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 39c074d4ff..c513f39f2d 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -67,7 +67,7 @@ module Info : sig
     (** Info for special constants *)
     -> ?scope : DeclareDef.locality
     (** locality  *)
-    -> ?kind:Decls.goal_object_kind
+    -> ?kind:Decls.logical_kind
     (** Theorem, etc... *)
     -> unit
     -> t
@@ -100,7 +100,7 @@ val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
   -> poly:bool
   -> scope:DeclareDef.locality
-  -> kind:Decls.goal_object_kind
+  -> kind:Decls.logical_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
   -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
@@ -115,7 +115,7 @@ val start_lemma_com
   :  program_mode:bool
   -> poly:bool
   -> scope:DeclareDef.locality
-  -> kind:Decls.goal_object_kind
+  -> kind:Decls.logical_kind
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:DeclareDef.Hook.t
   -> Vernacexpr.proof_expr list
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 7e615c05b0..5d7e1ff9f6 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -397,8 +397,8 @@ let deps_remaining obls deps =
     deps []
 
 
-let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(DefinitionBody Definition))
-let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(Proof Lemma))
+let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(IsDefinition Definition))
+let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(IsProof Lemma))
 
 let kind_of_obligation o =
   match o with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 335075e1e0..c3ffc6fba0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -557,7 +557,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   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 ~poly ~scope:local ~kind:(Decls.DefinitionBody kind) ?hook [(name, pl), (bl, t)]
+  start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)]
 
 let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
@@ -580,7 +580,7 @@ let vernac_start_proof ~atts kind l =
   let scope = 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 ~poly:atts.polymorphic ~scope ~kind:(Decls.Proof kind) l
+  start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l
 
 let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->