diff options
| author | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
| commit | 61aeca9ca2a7c46b143b90583dfb84b037eccc5b (patch) | |
| tree | 936cab27bacc3bb779aff810be7b79425544f10d /plugins/derive | |
| parent | 6e5fee168d874b7b6fe7d5c8f4384661bf328d79 (diff) | |
| parent | c62aa0e9d0c33a70822e66a422d4c5926a8c8df7 (diff) | |
Merge PR #12372: [declare] Refactor constant information into a record.
Reviewed-by: SkySkimmer
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 11 | ||||
| -rw-r--r-- | plugins/derive/derive.mli | 2 |
2 files changed, 6 insertions, 7 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index e5665c59b8..027064b75f 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 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 + let info = Declare.Info.make ~poly ~kind () in + let lemma = Declare.Proof.start_derive ~name ~f ~info goals in + 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 |