From 318110f9f690689a33b432a809e6dc62292c46e1 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 1 Mar 2004 10:54:38 +0000
Subject: Protection d'un 'clear' qui peut etre dependant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5403 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/coq_omega.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 9ac5b2205..3ab5a6255 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1316,7 +1316,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
   let shift_left = 
     tclTHEN 
       (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
-      (clear [id]) 
+      (tclTRY (clear [id]))
   in
   if tac <> [] then
     let id' = new_identifier () in 
-- 
cgit v1.2.3