From 3cc45d57f6001d8c377825b9b940bc51fb3a96f7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 26 Nov 2017 04:30:07 +0100
Subject: [api] Remove aliases of `Evar.t`

There don't really bring anything, we also correct some minor nits
with the printing function.
---
 plugins/ssr/ssrcommon.ml            | 2 +-
 plugins/ssrmatching/ssrmatching.ml4 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 83b4547698..047ca509be 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -565,7 +565,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   if evlist = [] then 0, c0 else
   let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
   pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
-    (fun (k,_) -> str(Evd.string_of_existential k)) evlist));
+    (fun (k,_) -> Evar.print k) evlist));
   let evplist = 
     let depev = List.fold_left (fun evs (_,(_,t,_)) -> 
         let t = EConstr.of_constr t in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 276b7c8ab2..e63a05b781 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
-- 
cgit v1.2.3