package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val type_of : ?refresh:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types
val e_type_of : ?refresh:bool -> Environ.env -> Evd.evar_map ref -> EConstr.constr -> EConstr.types
  • deprecated Use [Typing.type_of]
  • deprecated Use [Typing.sort_of]
  • deprecated Use [Typing.check]
  • deprecated Use [Typing.solve_evars]
val check_allowed_sort : Environ.env -> Evd.evar_map -> Constr.pinductive -> EConstr.constr -> EConstr.constr -> unit
val check_type_fixpoint : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Name.t array -> EConstr.types array -> EConstr.unsafe_judgment array -> Evd.evar_map
val judge_of_prop : EConstr.unsafe_judgment
val judge_of_set : EConstr.unsafe_judgment