From 17ba18d81e5fe3dc153b1c12ac1b8daeb5474d48 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 May 2019 06:10:29 +0200
Subject: [lemmas] Turn Lemmas.info into a proper type with constructor.

Lemmas.info was a bit out of hand, as well as the parameters to the
`start_*` family. Most of the info is not needed and should hopefully
remain constrained to special cases, most callers only set the hook,
and obligations should be better served by a `start_obligation`
function soon.
---
 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 72ca5dc8c4..22e20e2c52 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -39,8 +39,8 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in
-  let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending in
+  let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in
+  let lemma = Lemmas.start_dependent_lemma ~name ~kind ~info goals in
   Lemmas.pf_map (Proof_global.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
   end) lemma
-- 
cgit v1.2.3