From 5f59ce47991758e833ac1079a055ed9a8dce6717 Mon Sep 17 00:00:00 2001
From: delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 13 Feb 2003 20:42:17 +0000
Subject: Correction d'un bug introduit dans le backtracking d'occurrence

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3677 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index eb29d67ed..50dab07ad 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1205,7 +1205,7 @@ and tactic_of_value vle g =
 
 (* Evaluation with FailError catching *)
 and eval_with_fail interp tac goal =
-  try 
+  try
     (match interp goal tac with
     | VTactic tac -> VRTactic (tac goal)
     | a -> a)
@@ -1297,7 +1297,7 @@ and match_context_interp ist g lr lmr =
     with
     | (FailError _) as e -> raise e
     | NextOccurrence _ -> raise No_match
-    | e when e = No_match or Logic.catchable_exception e ->
+    | e when is_match_catchable e ->
       apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
   let rec apply_match_context ist env goal nrs lex lpt = 
     begin
-- 
cgit v1.2.3