Module `Retyping`Source

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

Sourcetype retype_error

Sourceexception RetypeError of retype_error

Source

val get_type_of : 
  ?polyprop:bool ->
  ?lax:bool ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.types

Source

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

Source

val get_sort_of : 
  ?polyprop:bool ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  EConstr.ESorts.t

Source

val get_sort_family_of : 
  ?polyprop:bool ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  Sorts.family

Source

val get_judgment_of : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.unsafe_judgment

Makes an unsafe judgment from a constr

Source

val type_of_global_reference_knowing_parameters : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr array ->
  EConstr.types

Source

val type_of_global_reference_knowing_conclusion : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.types ->
  Evd.evar_map * EConstr.types

Source

val sorts_of_context : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.rel_context ->
  EConstr.ESorts.t list

Source

val expand_projection : 
  Environ.env ->
  Evd.evar_map ->
  Names.Projection.t ->
  EConstr.constr ->
  EConstr.constr list ->
  EConstr.constr

Source

val reinterpret_get_type_of : 
  src:Names.Id.t ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.types

Sourceval print_retype_error : retype_error -> Pp.t

Source

val relevance_of_term : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.ERelevance.t

Source

val relevance_of_type : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  EConstr.ERelevance.t

Sourceval relevance_of_sort : EConstr.ESorts.t -> EConstr.ERelevance.t

Source

val relevance_of_sort_family : 
  Evd.evar_map ->
  Sorts.family ->
  EConstr.ERelevance.t

Sourceval is_term_irrelevant : Environ.env -> Evd.evar_map -> Evd.econstr -> bool

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Retyping/index.html

Module `Retyping`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Retyping/index.html

Module RetypingSource

Module `Retyping`Source