diff options
| author | Emilio Jesus Gallego Arias | 2020-06-23 22:47:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:13 +0200 |
| commit | d9dca86f798ce11861f1a4715763cad1aae28e5a (patch) | |
| tree | ccf36789d7aa883fb227c90e957d2ceb2fb7098c /vernac/declare.mli | |
| parent | 4a2c8653c0b2f5e73db769a8ea6bf79b76086524 (diff) | |
[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.
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 38 |
1 files changed, 15 insertions, 23 deletions
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 |