diff options
| author | Emilio Jesus Gallego Arias | 2020-05-11 04:09:31 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-18 19:08:19 +0200 |
| commit | 5ae026cebc6c468373459af950533bee0c02501a (patch) | |
| tree | 48de5a6e626a6c1e3aa4bd9ede844cae24ab4648 /plugins/derive | |
| parent | c8b54d74bc7cf29cc04d0a3cedbf4a106f6e744c (diff) | |
[declare] Grand unification of the proof save path.
We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.
In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.
The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .
There are still some TODOs, that will be addressed in subsequent PRs:
- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]
List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:
- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index f09b35a6d1..e5665c59b8 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -40,7 +40,7 @@ let start_deriving f suchthat name : Lemmas.t = TNil sigma)))))) in - let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () 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 |