LogicLegacy proof engine. Do not use in newly written code.
check respectively means:\\ Intro: check that the name does not exist\\ Intro_after: check that the name does not exist and that variables in its type does not escape their scope\\ Intro_replacing: check that the name does not exist and that variables in its type does not escape their scope\\ Convert_hyp: check that the name exist and that its type is convertible\\
type refiner_error = | BadType of Constr.constr * Constr.constr * EConstr.t |
| UnresolvedBindings of Names.Name.t list |
| CannotApply of Constr.constr * Constr.constr |
| NonLinearProof of Constr.constr |
| MetaInType of EConstr.constr |
| IntroNeedsProduct |
| NoSuchHyp of Names.Id.t |
exception RefinerError of Environ.env * Evd.evar_map * refiner_errorval error_no_such_hypothesis : Environ.env -> Evd.evar_map -> Names.Id.t -> 'aMove destination for hypothesis
val pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.tval convert_hyp : check:bool -> reorder:bool -> Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Environ.named_context_valexception CannotMoveHyp of cannot_move_hypval move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Names.Id.t -> Names.Id.t move_location -> Environ.named_context_val -> Environ.named_context_valval insert_decl_in_named_context : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Names.Id.t move_location -> Environ.named_context_val -> Environ.named_context_val