From 7b74581cd633d28c83589dff1adf060fcfe87e8a Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 27 Jun 2008 15:27:30 +0000
Subject: Changement de catch_error pour qu'il rattrape les erreurs d'arguments
 implicites. On peut désormais utiliser le fait que des arguments implicites
 ne sont pas inférés pour backtracker dans des preuves. C'est utile en
 particulier avec les typeclasses, mais peut servir dans d'autres cas.

Le code suivant ne fait donc aucune erreur :

Definition toto {x:True} := True.

Goal True.
  try apply toto.





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11183 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 654bc504a9..74c2a4befc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -53,7 +53,8 @@ let rec catchable_exception = function
   (* unification errors *)
   | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
-		   |CannotFindWellTypedAbstraction _)) -> true
+		   |CannotFindWellTypedAbstraction _
+		   |UnsolvableImplicit _)) -> true
   | _ -> false
 
 (* Tells if the refiner should check that the submitted rules do not
-- 
cgit v1.2.3