diff options
| author | Gaëtan Gilbert | 2020-03-31 11:05:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 11:05:21 +0200 |
| commit | 29bcd98d55ccb9a90dff7fc8f254578c4d870a09 (patch) | |
| tree | c87bee672d196212e4f0033804e57c00deadeef8 /vernac/comDefinition.mli | |
| parent | c31a634b1f57028f3491b61137e53978d2653bbe (diff) | |
| parent | 1320d5004b58f33c2274bfdc0629d7f513cd49c4 (diff) | |
Merge PR #11818: [proof] Further consolidation of the regular declaration path
Ack-by: Matafou
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac/comDefinition.mli')
| -rw-r--r-- | vernac/comDefinition.mli | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 6c6da8952e..337da22018 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -15,8 +15,7 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : program_mode:bool - -> ?hook:DeclareDef.Hook.t + : ?hook:DeclareDef.Hook.t -> name:Id.t -> scope:DeclareDef.locality -> poly:bool @@ -28,18 +27,15 @@ val do_definition -> constr_expr option -> unit -(************************************************************************) -(** Internal API *) -(************************************************************************) - -(** Not used anywhere. *) -val interp_definition - : program_mode:bool +val do_definition_program + : ?hook:DeclareDef.Hook.t + -> name:Id.t + -> scope:DeclareDef.locality + -> poly:bool + -> kind:Decls.definition_object_kind -> universe_decl_expr option -> local_binder_expr list - -> poly:bool -> red_expr option -> constr_expr -> constr_expr option - -> Evd.side_effects Declare.proof_entry * - Evd.evar_map * UState.universe_decl * Impargs.manual_implicits + -> unit |