diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 01:57:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | a2ea73d84be2fe95eeda42f5f5ac458f0af9968f (patch) | |
| tree | 0b3c485f6e196bb74dca8c2eda6a6cf2448b2745 /plugins | |
| parent | 5d18dfed8e68dd964bca5d64ca6bdd9f8ffbb1df (diff) | |
[proofs] Store hooks in the proof object.
As of now, hooks were stored in the terminators as closures, we place
them instead in the proof object and are thus passed back at proof
closing time.
This helps towards the reification and unification of terminators.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/derive/derive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index aad3967f6d..f8b5f455d1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -56,9 +56,9 @@ let start_deriving f suchthat name : Lemmas.t = let (opaque,f_def,lemma_def) = match com with | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Lemmas.Proved (_,Some _,_) -> + | Lemmas.Proved (_,Some _,_, _) -> CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Lemmas.Proved (opaque, None, obj) -> + | Lemmas.Proved (opaque, None, obj,_) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> opaque <> Proof_global.Transparent , f_def , lemma_def |