From 176f40f976741c8fb6e020c0eaeac4df59a474bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Jun 2014 10:33:40 +0200
Subject: Improved error message when a meta posed as an evar remains unsolved
 in case prefix 'e' of "apply" and co is not given.

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

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index db74e5aa18..41ce6f1da0 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -498,6 +498,8 @@ let explain_evar_kind env evi = function
       str "the type of an impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ ->
       assert false
+  | Evar_kinds.VarInstance id ->
+      str "an instance for the variable " ++ pr_id id
 
 let explain_unsolvability = function
   | None -> mt()
-- 
cgit v1.2.3