diff options
| author | Emilio Jesus Gallego Arias | 2020-02-29 15:25:42 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-12 20:36:36 -0400 |
| commit | 79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 (patch) | |
| tree | 5601c7ed11caa7e109edb2e462aa8e590303406b /vernac/declareDef.mli | |
| parent | c9f7a31ef67ce638ec591f9e5760941706bc12bc (diff) | |
[lemmas] Handle mutual lemmas more uniformly.
We split the paths for mutual / non-mutual constants, and we enforce
some further invariants, in particular we avoid messing around with
the body of saved constants, and using the indirect accessor.
This should be almost semantically equivalent to the previous code,
including some questionable choices present there.
In further cleanups we will move this code to Declare, which should
hopefully help clarify some of the semantics.
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 786169f409..17c2862cad 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -44,7 +44,6 @@ val declare_definition -> scope:locality -> kind:Decls.logical_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> ?should_suggest:bool -> UnivNames.universe_binders -> Evd.side_effects Declare.proof_entry -> Impargs.manual_implicits |