package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
doc/coq-core.pretyping/Retyping/index.html
Module RetypingSource
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
Source
val get_type_of :
?polyprop:bool ->
?lax:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.typesSource
val get_type_of_constr :
?polyprop:bool ->
?lax:bool ->
Environ.env ->
?uctx:UState.t ->
Constr.t ->
Constr.typesNo-evar version of get_type_of
Source
val get_sort_family_of :
?polyprop:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
Sorts.familySource
val get_judgment_of :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.unsafe_judgmentMakes 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.typesSource
val type_of_global_reference_knowing_conclusion :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.types ->
Evd.evar_map * EConstr.typesSource
val expand_projection :
Environ.env ->
Evd.evar_map ->
Names.Projection.t ->
EConstr.constr ->
EConstr.constr list ->
EConstr.constr