From 34bb77c953e917f5fbff489c5758abcbadc22224 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 3 Dec 2014 14:48:09 +0100
Subject: Slight improving of a unification error message.

---
 toplevel/himsg.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 421a975f17..9aa1486405 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -293,8 +293,9 @@ let explain_unification_error env sigma p1 p2 = function
     | InstanceNotSameType (evk,env,t,u) ->
         let t, u = pr_explicit env sigma t u in
         spc () ++ str "(unable to find a well-typed instantiation for " ++
-        quote (pr_existential_key sigma evk) ++ strbrk ": cannot unify " ++
-        t ++ strbrk " and " ++ u ++ str ")"
+        quote (pr_existential_key sigma evk) ++
+        strbrk ": cannot ensure that " ++
+        t ++ strbrk " is a subtype of " ++ u ++ str ")"
     | UnifUnivInconsistency p ->
         if !Constrextern.print_universes then
 	  spc () ++ str "(Universe inconsistency: " ++ 
-- 
cgit v1.2.3