From f5e644a53c69392f94eae01dd71ab79b4700a892 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 17 Feb 2013 14:56:11 +0000
Subject: A more informative message when the elimination predicate for
 destruct, rewrite, etc. is not well-typed.

Also added support for a more informative message when the elimination
predicate is not well-formed while using the smart "second-order"
unification algorithm. However the "abstract_list_all" algorithm seems
to remain more informative though, so we still use this algorithm for
reporting about ill-typed predicates.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c2ded73ad1..be5eb5dbdd 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -651,6 +651,8 @@ let set_solve_evars f = solve_evars := f
  * proposition from Dan Grayson]
  *)
 
+exception TypingFailed of evar_map
+
 let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   try
   let args = Array.to_list args in
@@ -702,10 +704,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
 
   (* We instantiate the evars of which the value is forced by typing *)
   let evd,rhs =
-    try !solve_evars env_evar evd rhs
+    let evdref = ref evd in
+    try let c = !solve_evars env_evar evdref rhs in !evdref,c
     with e when Pretype_errors.precatchable_exception e ->
       (* Could not revert all subterms *)
-      raise Exit in
+      raise (TypingFailed !evdref) in
 
   let rec abstract_free_holes evd = function
   | (id,idty,c,_,evsref,_,_)::l ->
@@ -736,7 +739,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       Evd.define evk rhs evd in
 
   abstract_free_holes evd subst, true
-  with Exit -> evd, false
+  with TypingFailed evd -> Evd.define evk rhs evd, false
 
 let second_order_matching_with_args ts env evd ev l t =
 (*
-- 
cgit v1.2.3