[declare] Remove Proof_ending from the public API

This completes the refactoring [for now] of the core `Declare`
interface, and will allow much internal refactoring in the future.

In particular, we remove the low-level Proof_ending type, and instead
introduce higher-level constructors for the several declare users.

Future PRs will change the internal representation of proof handling
to better enforce some invariants that should hold for specific
proofs.

3 files changed, 29 insertions, 28 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 27df963e98..027064b75f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -41,7 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t =
   in
 
   let info = Declare.Info.make ~poly ~kind () in
-  let proof_ending = Declare.Proof_ending.(End_derive {f; name}) in
-  let lemma = Declare.Proof.start_dependent ~name ~info ~proof_ending goals in
+  let lemma = Declare.Proof.start_derive ~name ~f ~info goals in
   Declare.Proof.map lemma ~f:(fun p ->
       Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 514656a414..d170e084d4 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1435,13 +1435,15 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof
 (** [start_proof ~info ~cinfo sigma] starts a proof of [cinfo].
    The proof is started in the evar map [sigma] (which
    can typically contain universe constraints) *)
-let start ~info ~cinfo ?proof_ending sigma =
+let start_core ~info ~cinfo ?proof_ending sigma =
   let { CInfo.name; typ; _ } = cinfo in
   let cinfo = [{ cinfo with CInfo.typ = EConstr.Unsafe.to_constr cinfo.CInfo.typ }] in
   let pinfo = Proof_info.make ~cinfo ~info ?proof_ending () in
   start_proof_core ~name ~typ ~pinfo ?sign:None sigma
 
-let start_dependent ~info ~name goals ~proof_ending =
+let start = start_core ?proof_ending:None
+
+let start_dependent ~info ~name ~proof_ending goals =
   let proof = Proof.dependent_start ~name ~poly:info.Info.poly goals in
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
   let cinfo = [] in
@@ -1453,6 +1455,14 @@ let start_dependent ~info ~name goals ~proof_ending =
   ; pinfo
   }
 
+let start_derive ~f ~name ~info goals =
+  let proof_ending = Proof_ending.End_derive {f; name} in
+  start_dependent ~info ~name ~proof_ending goals
+
+let start_equations ~name ~info ~hook ~types sigma goals =
+  let proof_ending = Proof_ending.End_equations {hook; i=name; types; sigma} in
+  start_dependent ~name ~info ~proof_ending goals
+
 let rec_tac_initializer finite guard thms snl =
   if finite then
     match List.map (fun { CInfo.name; typ } -> name, (EConstr.of_constr typ)) thms with
@@ -2238,7 +2248,7 @@ let rec solve_obligation prg num tac =
   let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in
   let poly = Internal.get_poly prg in
   let info = Info.make ~scope ~kind ~poly () in
-  let lemma = Proof.start ~cinfo ~info ~proof_ending evd  in
+  let lemma = Proof.start_core ~cinfo ~info ~proof_ending evd  in
   let lemma = fst @@ Proof.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in
   lemma
diff --git a/vernac/declare.mli b/vernac/declare.mli
index b6efa333b7..55bbcb9e1e 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -162,22 +162,6 @@ type obligation_resolver =
 
 type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
 
-(** Creating high-level proofs with an associated constant *)
-module Proof_ending : sig
-
-  type t =
-    | Regular
-    | End_obligation of obligation_qed_info
-    | End_derive of { f : Id.t; name : Id.t }
-    | End_equations of
-        { hook : Constant.t list -> Evd.evar_map -> unit
-        ; i : Id.t
-        ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
-        ; sigma : Evd.evar_map
-        }
-
-end
-
 (** [Declare.Proof.t] Construction of constants using interactive proofs. *)
 module Proof : sig
 
@@ -189,19 +173,27 @@ module Proof : sig
   val start
     :  info:Info.t
     -> cinfo:EConstr.t CInfo.t
-    -> ?proof_ending:Proof_ending.t
     -> Evd.evar_map
     -> t
 
-  (** Like [start] except that there may be dependencies between initial goals. *)
-  val start_dependent
-    : info:Info.t
-    -> name:Id.t
+  (** [start_{derive,equations}] are functions meant to handle
+     interactive proofs with multiple goals, they should be considered
+     experimental until we provide a more general API encompassing
+     both of them. Please, get in touch with the developers if you
+     would like to experiment with multi-goal dependent proofs so we
+     can use your input on the design of the new API. *)
+  val start_derive : f:Id.t -> name:Id.t -> info:Info.t -> Proofview.telescope -> t
+
+  val start_equations :
+       name:Id.t
+    -> info:Info.t
+    -> hook:(Constant.t list -> Evd.evar_map -> unit)
+    -> types:(Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
+    -> Evd.evar_map
     -> Proofview.telescope
-    -> proof_ending:Proof_ending.t
     -> t
 
-  (** Pretty much internal, used by the Lemmavernaculars *)
+  (** Pretty much internal, used by the Lemma vernaculars *)
   val start_with_initialization
     :  info:Info.t
     -> cinfo:Constr.t CInfo.t