From cb84805a1758ab52506f74207dacd80a8f07224e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 14 Feb 2019 12:45:49 +0100
Subject: [save_proof] Make terminator API internal.

We refactor the terminator API to make it more internal. Indeed we
remove `set_terminator` and `get_terminator` is only there due to
access to internals in the STM `save_proof` path by the infamous
`?proof` parameter.

After this only 2 non-standard terminators remain: obligations and
derive. We will refactor those in next PRs.
---
 plugins/derive/derive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index fd5b3a7e48..cff8214438 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -99,7 +99,7 @@ let start_deriving f suchthat name : Lemmas.t =
       ignore (Declare.declare_constant name lemma_def)
   in
 
-  let terminator ?hook _ = Lemmas.make_terminator terminator in
+  let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in
   let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
   Lemmas.simple_with_proof begin fun _ p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
-- 
cgit v1.2.3