From 2ac8e0edebe0d9a6bde4d997327dbd2ffcde08b6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 4 Jun 2014 15:42:41 +0200
Subject: - Allow parsing of @const@{instance} for specifying universe
 instances of polymorphic constants.

---
 toplevel/himsg.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 9d6e9756dd..db74e5aa18 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -861,7 +861,11 @@ let explain_unsatisfiable_constraints env evd constr comp =
   | None -> Typeclasses.is_resolvable evi
   | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp
   in
-  let undef = Evar.Map.filter is_kept undef in
+  let undef = 
+    let m = Evar.Map.filter is_kept undef in
+      if Evar.Map.is_empty m then undef
+      else m
+  in
   match constr with
   | None ->
     str "Unable to satisfy the following constraints:" ++ fnl () ++
-- 
cgit v1.2.3