aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
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 /engine/evd.ml
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 'engine/evd.ml')
-rw-r--r--engine/evd.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 60bd6de2a..ecef04204 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -127,7 +127,7 @@ end
module Store = Store.Make ()
-type evar = existential_key
+type evar = Evar.t
let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
@@ -371,7 +371,7 @@ val key : Id.t -> t -> Evar.t
end =
struct
-type t = Id.t EvMap.t * existential_key Id.Map.t
+type t = Id.t EvMap.t * Evar.t Id.Map.t
let empty = (EvMap.empty, Id.Map.empty)