Logic (rocq-runtime.Logic)

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 =

| 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_error

val error_no_such_hypothesis : Environ.env -> Evd.evar_map -> Names.Id.t -> 'a

type 'id move_location =

| MoveAfter of 'id
(*
Move to the position directly _after_ a hypothesis.
*)
| MoveBefore of 'id
(*
Move to the position directly _before_ a hypothesis.
*)
| MoveFirst
(*
Move to the first position in the context.
*)
| MoveLast
(*
Move to the last position in the context. This is the default used by intro.
*)

Move destination for hypothesis.

val pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.t

Print a move_location.

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 ->
  (Environ.var_status * EConstr.named_declaration) ->
  Names.Id.t move_location ->
  Environ.named_context_val ->
  Environ.named_context_val