package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val refiner : check:bool -> Constr.constr -> unit Proofview.tactic
type refiner_error =
  1. | BadType of Constr.constr * Constr.constr * EConstr.t
  2. | UnresolvedBindings of Names.Name.t list
  3. | CannotApply of Constr.constr * Constr.constr
  4. | NonLinearProof of Constr.constr
  5. | MetaInType of EConstr.constr
  6. | IntroNeedsProduct
  7. | 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 =
  1. | MoveAfter of 'id
  2. | MoveBefore of 'id
  3. | MoveFirst
  4. | MoveLast
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