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/declare.mli | |
| 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/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 9 |
1 files changed, 1 insertions, 8 deletions
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 |