diff options
| author | Gaëtan Gilbert | 2020-03-22 11:07:58 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-22 11:07:58 +0100 |
| commit | 7ba059507b67b1f6ea3566a5d1dee40f6af78316 (patch) | |
| tree | cb901254b587eabdb2c508fdf60a9bbc23971920 /vernac/declareDef.mli | |
| parent | b048ecb6d874e1eb2e33c1fa3a15d3a508500285 (diff) | |
| parent | c3350ed82e1dd4e299a5a14e6e63103556a379d2 (diff) | |
Merge PR #11731: [proof] Miscellaneous refactorings
Reviewed-by: SkySkimmer
Reviewed-by: gares
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 |