diff options
Diffstat (limited to 'plugins/derive/derive.ml')
| -rw-r--r-- | plugins/derive/derive.ml | 9 |
1 files changed, 4 insertions, 5 deletions
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) |