From 8ac929ea128f1f7353b3f4d532b642e769542e55 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 17 Feb 2013 14:56:04 +0000
Subject: Added propagation of evars unification failure reasons for better
 error messages. The architecture of unification error handling changed, not
 helped by ocaml for checking that every exceptions is correctly caught.
 Report or fix if you find a regression.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/printer.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 7a9dcb03cd..fa776d11e0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -127,6 +127,7 @@ let pr_global_env = pr_global_env
 let pr_global = pr_global_env Id.Set.empty
 
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
+let pr_existential_key evk = str (string_of_existential evk)
 let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
 let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
 let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
-- 
cgit v1.2.3