From d8e39f445103466b36a2c04cca52ddb880d9cae7 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 16 Apr 2013 18:36:36 +0000
Subject: Fixing #2968. This is quite brittle though, because we are messing
 with the exception catching system of Ltac which is not really known for its
 safety, so that it may break a few things.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16411 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 354935aa8c..7ec1b684bb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -40,20 +40,29 @@ exception RefinerError of refiner_error
 
 open Pretype_errors
 
+(** FIXME: this is quite brittle. Why not accept any PretypeError? *)
+let is_typing_error = function
+| UnexpectedType (_, _) | NotProduct _
+| VarNotFound _ | TypingError _ -> true
+| _ -> false
+
+let is_unification_error = function
+| CannotUnify _ | CannotUnifyLocal _| CannotGeneralize _
+| NoOccurrenceFound _ | CannotUnifyBindingType _
+| ActualTypeNotCoercible _ | UnifOccurCheck _
+| CannotFindWellTypedAbstraction _ | WrongAbstractionType _
+| UnsolvableImplicit _| AbstractionOverMeta _ -> true
+| _ -> false
+
 let rec catchable_exception = function
   | LtacLocated(_,_,e) -> catchable_exception e
-  | Errors.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
+  | Errors.UserError _ | TypeError _
   | RefinerError _ | Indrec.RecursionSchemeError _
-  | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
+  | Nametab.GlobalizationError _
   (* reduction errors *)
-  | Tacred.ReductionTacticError _ 
-  (* unification errors *)
-  | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
-		   |NoOccurrenceFound _|CannotUnifyBindingType _
-		   |ActualTypeNotCoercible _|UnifOccurCheck _
-                   |CannotFindWellTypedAbstraction _
-		   |WrongAbstractionType _
-		   |UnsolvableImplicit _|AbstractionOverMeta _)) -> true
+  | Tacred.ReductionTacticError _ -> true
+  (* unification and typing errors *)
+  | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e
   | Typeclasses_errors.TypeClassError
       (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
   | _ -> false
-- 
cgit v1.2.3