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 /plugins/derive | |
| 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 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 3 |
1 files changed, 1 insertions, 2 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) |