Module `Logic`

Legacy proof engine. Do not use in newly written code.

val refiner : check:bool -> Constr.constr -> unit Proofview.tactic

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

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

val 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_val
val 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