diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 02:26:43 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:16:22 -0400 |
| commit | b755869a7fdb34dcf7dacc9d5fd93c768d71d751 (patch) | |
| tree | 68eb026dc0f9e214afcb44739e2c617d3d5f8be6 /plugins | |
| parent | 5828dffb05022ff667f44b1ad9a89f677647e0b4 (diff) | |
[proof] Split delayed and regular proof closing functions, part II
We make the types of the delayed / non-delayed declaration path
different, as the latter is just creating futures that are forced
right away.
TTBOMK the new code should behave identically w.r.t. old one, modulo
the equation `Future.(force (from_val x)) = x`.
There are some questions as what the code is doing, but in this PR
I've opted to keep the code 100% faithful to the original one, unless
I did a mistake.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/gen_principle.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 45c46c56f4..0ed04d262a 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_ (* end; *) let open Proof_global in - let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma in match entries with | [entry] -> entry, hook |