From 15afb8a58f29f45cae6a6abca5426abc524408dd Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 19 Oct 2002 09:31:10 +0000
Subject: Réparation bug #180
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 6b6efb807..47893c093 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1664,7 +1664,11 @@ let destructure_hyps gl =
 		    (intros_using [i1;i2]))
 		 (loop (i1::i2::evbd) ((i1,None,t1)::(i2,None,t2)::lit)))
           | Kimp(t1,t2) ->
-              if isprop (pf_type_of gl t1) & closed0 t2 then begin
+              if
+                is_Prop (pf_type_of gl t1) &
+                is_Prop (pf_type_of gl t2) &
+                closed0 t2
+              then
 		(tclTHEN 
 		   (tclTHEN 
 		      (tclTHEN
@@ -1675,7 +1679,7 @@ let destructure_hyps gl =
 			 (clear [i])) 
 		      (intros_using [i])) 
 		   (loop evbd ((i,None,mk_or (mk_not t1) t2)::lit)))
-              end else
+              else
 		loop evbd lit
           | Kapp("not",[t]) -> 
               begin match destructurate t with 
-- 
cgit v1.2.3