package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module ESorts : sig ... end
module EInstance : sig ... end
type t = econstr
val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type
val whd_evar : evar_map -> t -> t
val of_constr : Constr.t -> t
val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
val unsafe_to_constr : t -> Constr.t
val unsafe_eq : (t, Constr.t) Util.eq