diff options
| author | Emilio Jesus Gallego Arias | 2020-05-22 03:55:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-26 18:26:47 +0200 |
| commit | 946c6c7e58a1dfbe57445a0a1508a587193bb7c3 (patch) | |
| tree | d5deba68d2f2cba0d0497233538b397924571898 /vernac | |
| parent | 1eb5f0504561224affd93717a9fca0e3162dcdd9 (diff) | |
[declare] Simplify exported type of definition_entry
This reduces the amount of exported internals, in particular
w.r.t. proof delaying and side effects which we will need in future
refactorings.
Actually turning the type from `Evd.side_effects proof_entry` to `unit
proof_entry` is left for the next commits.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declare.ml | 11 | ||||
| -rw-r--r-- | vernac/declare.mli | 9 |
2 files changed, 9 insertions, 11 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index c77d4909da..7394f7f9c2 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -138,7 +138,9 @@ type 'a proof_entry = { let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types +(** [univsbody] are universe-constraints attached to the body-only, + used in vio-delayed opaque constants and private poly universes *) +let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); proof_entry_secctx = section_vars; @@ -148,6 +150,9 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?sect proof_entry_feedback = feedback_id; proof_entry_inline_code = inline} +let definition_entry = + definition_entry_core ?fix_exn:None ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None + type proof_object = { name : Names.Id.t (* [name] only used in the STM *) @@ -241,7 +246,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = let utyp = UState.check_univ_decl ~poly ctx udecl in utyp, Univ.ContextSet.empty in - definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body + definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body in let entries = CList.map make_entry elist in { name; entries; uctx } @@ -998,7 +1003,7 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in - let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in + let entry = definition_entry_core ?fix_exn ?opaque ?inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in entry, uctx diff --git a/vernac/declare.mli b/vernac/declare.mli index 647896e2f5..b380afc97d 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -144,17 +144,10 @@ val declare_variable for removal from the public API, use higher-level declare APIs instead *) val definition_entry - : ?fix_exn:Future.fix_exn - -> ?opaque:bool + : ?opaque:bool -> ?inline:bool - -> ?feedback_id:Stateid.t - -> ?section_vars:Id.Set.t -> ?types:types -> ?univs:Entries.universes_entry - -> ?eff:Evd.side_effects - -> ?univsbody:Univ.ContextSet.t - (** Universe-constraints attached to the body-only, used in - vio-delayed opaque constants and private poly universes *) -> constr -> Evd.side_effects proof_entry |