Retyping
This family of functions assumes its constr argument is known to be well-typable. It does not type-check, just recompute the type without any costly verifications. On non well-typable terms, it either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too.
The "polyprop" optional argument is used by the extraction to disable "Prop-polymorphism", cf comment in inductive.ml
The "lax" optional argument provides a relaxed version of get_type_of
that won't raise any anomaly but RetypeError instead
exception RetypeError of retype_error
val get_type_of :
?polyprop:bool ->
?lax:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.types
val get_type_of_constr :
?polyprop:bool ->
?lax:bool ->
Environ.env ->
?uctx:UState.t ->
Constr.t ->
Constr.types
No-evar version of get_type_of
val get_sort_of :
?polyprop:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
EConstr.ESorts.t
val get_sort_family_of :
?polyprop:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
Sorts.family
val get_judgment_of :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.unsafe_judgment
Makes an unsafe judgment from a constr
val type_of_global_reference_knowing_parameters :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.constr array ->
EConstr.types
val type_of_global_reference_knowing_conclusion :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.types ->
Evd.evar_map * EConstr.types
val sorts_of_context :
Environ.env ->
Evd.evar_map ->
EConstr.rel_context ->
EConstr.ESorts.t list
val expand_projection :
Environ.env ->
Evd.evar_map ->
Names.Projection.t ->
EConstr.constr ->
EConstr.constr list ->
EConstr.constr
val reinterpret_get_type_of :
src:Names.Id.t ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.types
val print_retype_error : retype_error -> Pp.t
val relevance_of_term :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
Sorts.relevance
val relevance_of_type :
Environ.env ->
Evd.evar_map ->
EConstr.types ->
Sorts.relevance
val relevance_of_sort : Evd.evar_map -> EConstr.ESorts.t -> Sorts.relevance
val relevance_of_sort_family : Evd.evar_map -> Sorts.family -> Sorts.relevance