aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
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 /plugins/ssrmatching
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 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 276b7c8ab..e63a05b78 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -396,7 +396,7 @@ let inv_dir = function L2R -> R2L | R2L -> L2R
type pattern_class =
| KpatFixed
| KpatConst
- | KpatEvar of existential_key
+ | KpatEvar of Evar.t
| KpatLet
| KpatLam
| KpatRigid