package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.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"
The "lax" optional argument provides a relaxed version of get_type_of that won't raise any anomaly but RetypeError instead
val get_type_of :
?metas:(Constr.metavariable -> EConstr.types option) ->
?polyprop:bool ->
?lax:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.typesval get_type_of_constr :
?polyprop:bool ->
?lax:bool ->
Environ.env ->
?uctx:UState.t ->
Constr.t ->
Constr.typesNo-evar version of get_type_of
val get_sort_of :
?polyprop:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
EConstr.ESorts.tval get_sort_family_of :
?polyprop:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
Sorts.familyval get_judgment_of :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.unsafe_judgmentMakes an unsafe judgment from a constr
val type_of_global_reference_knowing_parameters :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.constr array ->
EConstr.typesval type_of_global_reference_knowing_conclusion :
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.types ->
Evd.evar_map * EConstr.typesval sorts_of_context :
Environ.env ->
Evd.evar_map ->
EConstr.rel_context ->
EConstr.ESorts.t listval expand_projection :
Environ.env ->
Evd.evar_map ->
Names.Projection.t ->
EConstr.constr ->
EConstr.constr list ->
EConstr.constrval reinterpret_get_type_of :
src:Names.Id.t ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.typesval relevance_of_projection_repr :
Environ.env ->
Names.Projection.Repr.t EConstr.puniverses ->
EConstr.ERelevance.tThe "polyprop" optional argument above controls the "Prop-polymorphism". By default, it is allowed. But when "polyprop=false", the following exception is raised when a polymorphic singleton inductive type becomes Prop due to parameter instantiation. This is used by the Ocaml extraction, which cannot handle (yet?) Prop-polymorphism.