diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 01:00:56 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:07 -0400 |
| commit | 069304b4e3ba75c54e372615bf7bb0ee2a103b5d (patch) | |
| tree | 3b959be77f58ec8c1550310983ff592f9f6fd33c /vernac/declareDef.mli | |
| parent | 9f680f776140c8b3b8f79013262d5bd73761d571 (diff) | |
[declare] Bring more consistency to parameters using labels
Most of the parameters were named, we fix the remaining cases.
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1ff2145c0d..fb1fc9242c 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -44,9 +44,9 @@ val declare_definition -> scope:locality -> kind:Decls.logical_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> UnivNames.universe_binders + -> ubind:UnivNames.universe_binders + -> impargs:Impargs.manual_implicits -> Evd.side_effects Declare.proof_entry - -> Impargs.manual_implicits -> GlobRef.t val declare_assumption @@ -64,12 +64,16 @@ val prepare_definition -> ?opaque:bool -> ?inline:bool -> poly:bool - -> Evd.evar_map - -> UState.universe_decl + -> udecl:UState.universe_decl -> types:EConstr.t option -> body:EConstr.t + -> Evd.evar_map -> Evd.evar_map * Evd.side_effects Declare.proof_entry -val prepare_parameter : allow_evars:bool -> - poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> - Evd.evar_map * Entries.parameter_entry +val prepare_parameter + : allow_evars:bool + -> poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.types + -> Evd.evar_map + -> Evd.evar_map * Entries.parameter_entry |