Module ComAssumption

Parameters/Assumptions
val 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_implicits
val do_assumptions : program_mode:bool -> poly:bool -> scope:Locality.definition_scope -> kind:Decls.assumption_object_kind -> ?⁠deprecation:Deprecation.t -> Declaremods.inline -> (Constrexpr.ident_decl list * Constrexpr.constr_expr) Vernacexpr.with_coercion list -> unit
val 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 -> unit
val declare_axiom : Vernacexpr.coercion_flag -> local:Locality.import_status -> kind:Decls.assumption_object_kind -> ?⁠deprecation:Deprecation.t -> Constr.types -> UState.named_universes_entry -> Impargs.manual_implicits -> Declaremods.inline -> Names.variable CAst.t -> Names.GlobRef.t * UVars.Instance.t
val do_context : poly:bool -> Constrexpr.local_binder_expr list -> unit
val 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) list

The first half of the context command, from expr to constr