From 7fd28dc95e3251a10617ddb6758cc00b8960f954 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Mar 2018 13:19:13 +0100
Subject: Slightly refining some error messages about unresolvable evars.

For instance, error in "Goal forall a f, f a = 0" is now located.
---
 intf/evar_kinds.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml
index c5de383b21..c964ecf1f5 100644
--- a/intf/evar_kinds.ml
+++ b/intf/evar_kinds.ml
@@ -21,6 +21,8 @@ type obligation_definition_status = Define of bool | Expand
 
 type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
 
+type subevar_kind = Domain | Codomain | Body
+
 type t =
   | ImplicitArg of global_reference * (int * Id.t option)
      * bool (** Force inference *)
@@ -34,4 +36,4 @@ type t =
   | ImpossibleCase
   | MatchingVar of matching_var_kind
   | VarInstance of Id.t
-  | SubEvar of Evar.t
+  | SubEvar of subevar_kind option * Evar.t
-- 
cgit v1.2.3