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 = | UnresolvedBindings of Names.Name.t list |
| CannotApply of EConstr.t * EConstr.t |
| NonLinearProof of EConstr.t |
| 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