aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-26 04:30:07 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-26 04:33:51 +0100
commit3cc45d57f6001d8c377825b9b940bc51fb3a96f7 (patch)
treeffd95829dd19c019811e82f6c849213920849ff3 /pretyping/pretyping.mli
parentc1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff)
[api] Remove aliases of `Evar.t`
There don't really bring anything, we also correct some minor nits with the printing function.
Diffstat (limited to 'pretyping/pretyping.mli')
-rw-r--r--pretyping/pretyping.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index b2735ee22..838938524 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -27,7 +27,7 @@ val search_guard :
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type inference_hook = env -> evar_map -> evar -> evar_map * constr
+type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
type inference_flags = {
use_typeclasses : bool;