From 879475156ccbfb14687ed9a02b04f8cf2422d698 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 May 2019 17:29:22 +0200
Subject: [proof] Uniformize Proof_global API

We rename modify to map [more in line with the rest of the system] and
make the endline function specific, as it is only used in one case.
---
 plugins/derive/derive.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index cff8214438..79d1c7520f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -101,6 +101,6 @@ let start_deriving f suchthat name : Lemmas.t =
 
   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 ->
+  Lemmas.pf_map (Proof_global.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
-  end lemma
+  end) lemma
-- 
cgit v1.2.3