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

---
 pretyping/pretype_errors.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 99b5a51f93..9b5b79284b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -36,8 +36,7 @@ type pretype_error =
   | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
   (* Tactic unification *)
   | UnifOccurCheck of existential_key * constr
-  | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t *
-      Evd.unsolvability_explanation option
+  | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
   | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
@@ -107,9 +106,9 @@ let error_not_a_type_loc loc env sigma j =
 let error_occur_check env sigma ev c =
   raise (PretypeError (env, sigma, UnifOccurCheck (ev,c)))
 
-let error_unsolvable_implicit loc env sigma evi e explain =
+let error_unsolvable_implicit loc env sigma evk explain =
   Loc.raise loc
-    (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
+    (PretypeError (env, sigma, UnsolvableImplicit (evk, explain)))
 
 let error_cannot_unify_loc loc env sigma ?reason (m,n) =
   Loc.raise loc (PretypeError (env, sigma,CannotUnify (m,n,reason)))
-- 
cgit v1.2.3