From 34cb1f6491017e4ed1a509f6b83b88a812ac425f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 9 Dec 2014 12:09:44 +0100
Subject: Tentatively more informative report of failure when inferring
 pattern-matching predicate.

---
 intf/evar_kinds.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf/evar_kinds.mli')

diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index f77fc5a6a..aae6e95aa 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -21,11 +21,11 @@ type t =
      * bool (** Force inference *)
   | BinderType of Name.t
   | QuestionMark of obligation_definition_status
-  | CasesType
+  | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
   | MatchingVar of bool * Id.t
   | VarInstance of Id.t
-  | SubEvar of t
+  | SubEvar of Constr.existential_key
-- 
cgit v1.2.3