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 /tactics/declare.ml | |
| 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 'tactics/declare.ml')
| -rw-r--r-- | tactics/declare.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 5e6f78be6f..a149850a64 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -187,14 +187,14 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); - proof_entry_secctx = None; +let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univc=Univ.ContextSet.empty) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,univc), eff); + proof_entry_secctx = section_vars; proof_entry_type = types; proof_entry_universes = univs; proof_entry_opaque = opaque; - proof_entry_feedback = None; + proof_entry_feedback = feedback_id; proof_entry_inline_code = inline} let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types |