From d9dca86f798ce11861f1a4715763cad1aae28e5a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Jun 2020 22:47:53 +0200
Subject: [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.
---
 plugins/derive/derive.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

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)
-- 
cgit v1.2.3