aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 83b454769..047ca509b 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