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

4 files changed, 14 insertions, 31 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 98002de119..7af14d099c 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -112,14 +112,12 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
 
-open Decl_kinds
-
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaultBehavior, Proof Theorem) typ tac =
+let build_constant_by_tactic ~name ctx sign ~poly typ tac =
   let evd = Evd.from_ctx ctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof ~name:id ~poly ~udecl:UState.default_univ_decl ~kind:goal_kind evd goals in
+  let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
@@ -135,11 +133,9 @@ let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaul
     iraise reraise
 
 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 name = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let gk = Global ImportDefaultBehavior, Proof Theorem in
-  let ce, status, univs =
-    build_constant_by_tactic id sigma sign ~poly ~goal_kind:gk typ tac in
+  let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly 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 51cb3ca0ee..d1d20b9efe 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -59,11 +59,10 @@ val use_unification_heuristics : unit -> bool
     tactic. *)
 
 val build_constant_by_tactic
-  :  Id.t
+  :  name: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
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8ac4435539..59ece4296b 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -40,7 +40,6 @@ 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
   }
@@ -52,14 +51,12 @@ type t =
   ; section_vars : Constr.named_context option
   ; proof : Proof.t
   ; udecl: UState.universe_decl
-  ; strength : Decl_kinds.goal_kind
   }
 
 (*** Proof Global manipulation ***)
 
 let get_proof ps = ps.proof
 let get_proof_name ps = (Proof.data ps.proof).Proof.name
-let get_persistence ps = ps.strength
 
 let map_proof f p = { p with proof = f p.proof }
 let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
@@ -86,28 +83,23 @@ let compact_the_proof pf = map_proof Proof.compact pf
 let set_endline_tactic tac ps =
   { ps with endline_tactic = Some tac }
 
-(** [start_proof sigma id pl str goals] starts a proof of name
-    [id] with goals [goals] (a list of pairs of environment and
-    conclusion); [str] describes what kind of theorem/definition this
-    is (spiwack: for potential printing, I believe is used only by
-    closing commands and the xml plugin); [terminator] is used at the
-    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 ~name ~udecl ~poly ~kind sigma goals =
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion). The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
+let start_proof ~name ~udecl ~poly sigma goals =
   { proof = Proof.start ~name ~poly sigma goals
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
-  ; strength = kind
   }
 
-let start_dependent_proof ~name ~udecl ~poly ~kind goals =
+let start_dependent_proof ~name ~udecl ~poly goals =
   { proof = Proof.dependent_start ~name ~poly goals
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
-  ; strength = kind
   }
 
 let get_used_variables pf = pf.section_vars
@@ -162,7 +154,7 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; udecl; strength } = ps in
+  let { section_vars; proof; udecl } = ps in
   let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
@@ -256,7 +248,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; poly; persistence = strength; universes; udecl }
+  { id = name; entries = entries; poly; 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 2c328bcf12..b402008361 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -17,7 +17,6 @@ type t
 (* Should be moved into a proper view *)
 val get_proof : t -> Proof.t
 val get_proof_name : t -> Names.Id.t
-val get_persistence : t -> Decl_kinds.goal_kind
 val get_used_variables : t -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
@@ -47,7 +46,6 @@ 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
   }
@@ -66,7 +64,6 @@ val start_proof
   :  name:Names.Id.t
   -> udecl:UState.universe_decl
   -> poly:bool
-  -> kind:Decl_kinds.goal_kind
   -> Evd.evar_map
   -> (Environ.env * EConstr.types) list
   -> t
@@ -77,7 +74,6 @@ val start_dependent_proof
   :  name:Names.Id.t
   -> udecl:UState.universe_decl
   -> poly:bool
-  -> kind:Decl_kinds.goal_kind
   -> Proofview.telescope
   -> t