ComAssumptionval interp_assumption : program_mode:bool -> Environ.env -> Evd.evar_map -> Constrintern.internalization_env -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.t * Impargs.manual_implicitsval do_assumptions : program_mode:bool -> poly:bool -> scope:Locality.definition_scope -> kind:Decls.assumption_object_kind ->
Declaremods.inline -> (Constrexpr.ident_decl list * Constrexpr.constr_expr) Vernacexpr.with_coercion list -> unitval declare_variable : Vernacexpr.coercion_flag -> kind:Decls.assumption_object_kind -> Constr.types -> UState.named_universes_entry -> Impargs.manual_implicits -> Glob_term.binding_kind -> Names.variable CAst.t -> unitval declare_axiom : Vernacexpr.coercion_flag -> poly:bool -> local:Locality.import_status -> kind:Decls.assumption_object_kind -> Constr.types -> UState.named_universes_entry -> Impargs.manual_implicits -> Declaremods.inline -> Names.variable CAst.t -> Names.GlobRef.t * Univ.Instance.tContext command
val do_context : poly:bool -> Constrexpr.local_binder_expr list -> unitval interp_context : Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> Evd.evar_map * (Names.Id.t * Constr.t option * Constr.t * Glob_term.binding_kind) listThe first half of the context command, from expr to constr