diff options
Diffstat (limited to 'contrib/xml/doubleTypeInference.mli')
| -rw-r--r-- | contrib/xml/doubleTypeInference.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli index 2e0badbfb..a934eaa7e 100644 --- a/contrib/xml/doubleTypeInference.mli +++ b/contrib/xml/doubleTypeInference.mli @@ -1,5 +1,10 @@ type types = { synthesized : Term.types; expected : Term.types option; } +val cprop : Names.kernel_name + +val whd_betadeltaiotacprop : + Environ.env -> Evd.evar_map -> Term.constr -> Term.constr + val double_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr option -> types Acic.CicHash.t -> unit |