ComDefinitionval interp_definition : program_mode:bool ->
Environ.env -> Evd.evar_map -> Constrintern.internalization_env -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicitsval do_definition : ?loc:Loc.t -> ?hook:Declare.Hook.t -> name:Names.Id.t -> ?scope:Locality.definition_scope -> ?clearbody:bool -> poly:bool
-> ?typing_flags:Declarations.typing_flags -> kind:Decls.definition_object_kind -> ?using:Vernacexpr.section_subset_expr -> ?user_warns:Globnames.extended_global_reference UserWarn.with_qf ->
Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> unitval do_definition_program : ?loc:Loc.t -> ?hook:Declare.Hook.t -> pm:Declare.OblState.t -> name:Names.Id.t -> scope:Locality.definition_scope ->
?clearbody:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags -> kind:Decls.logical_kind -> ?using:Vernacexpr.section_subset_expr -> ?user_warns:Globnames.extended_global_reference UserWarn.with_qf ->
Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> Declare.OblState.tval do_definition_interactive : ?loc:Loc.t -> program_mode:bool -> ?hook:Declare.Hook.t -> name:Names.Id.t ->
scope:Locality.definition_scope -> ?clearbody:bool -> poly:bool -> typing_flags:Declarations.typing_flags option -> kind:Decls.logical_kind -> ?using:Vernacexpr.section_subset_expr ->
?user_warns:Globnames.extended_global_reference UserWarn.with_qf -> Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Declare.Proof.t