package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
  • deprecated Use [type_of] or retyping according to your needs.
val type_of : ?refresh:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types
val type_of_variable : Environ.env -> Names.variable -> EConstr.types
val check_type_fixpoint : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Name.t Context.binder_annot array -> EConstr.types array -> EConstr.unsafe_judgment array -> Evd.evar_map
val judge_of_sprop : EConstr.unsafe_judgment
val judge_of_prop : EConstr.unsafe_judgment
val judge_of_set : EConstr.unsafe_judgment
val judge_of_float : Environ.env -> Float64.t -> EConstr.unsafe_judgment