From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:09:30 +0200
Subject: [declare] Move proof information to declare.

At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
---
 plugins/derive/derive.ml  | 9 ++++-----
 plugins/derive/derive.mli | 2 +-
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e5665c59b8..633d5dfe3b 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -15,7 +15,7 @@ open Context.Named.Declaration
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
-let start_deriving f suchthat name : Lemmas.t =
+let start_deriving f suchthat name : Declare.Proof.t =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -40,8 +40,7 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
+  let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
   let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
-  Lemmas.pf_map (Declare.Proof.map_proof begin fun p ->
-    Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
-  end) lemma
+  Declare.Proof.map lemma ~f:(fun p ->
+      Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index ef94c7e78f..06e7dacd36 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -16,4 +16,4 @@ val start_deriving
   :  Names.Id.t
   -> Constrexpr.constr_expr
   -> Names.Id.t
-  -> Lemmas.t
+  -> Declare.Proof.t
-- 
cgit v1.2.3