summaryrefslogtreecommitdiff
path: root/contrib/xml/doubleTypeInference.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml/doubleTypeInference.mli')
-rw-r--r--contrib/xml/doubleTypeInference.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli
index 33d3e5cd..2e14b558 100644
--- a/contrib/xml/doubleTypeInference.mli
+++ b/contrib/xml/doubleTypeInference.mli
@@ -14,7 +14,7 @@
type types = { synthesized : Term.types; expected : Term.types option; }
-val cprop : Names.kernel_name
+val cprop : Names.constant
val whd_betadeltaiotacprop :
Environ.env -> Evd.evar_map -> Term.constr -> Term.constr