Module Logic

Legacy 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\\

Refiner errors.
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_error
val error_no_such_hypothesis : Environ.env -> Evd.evar_map -> Names.Id.t -> 'a

Move destination for hypothesis

type 'id move_location =
| MoveAfter of 'id
| MoveBefore of 'id
| MoveFirst
| MoveLast(*

can be seen as "no move" when doing intro

*)
val pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.t
val convert_hyp : check:bool -> reorder:bool -> Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Environ.named_context_val
type cannot_move_hyp
exception CannotMoveHyp of cannot_move_hyp