From 5b0f516e7e1f6d2ea8ca0485ffe347a613b01a5c Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 2 May 2000 20:49:25 +0000
Subject: portage Omega (mais toujours pas Zpower et Zlogarithm)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Bool/Bool.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'theories/Bool')

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 7f8f52c4f6..ab1a4b9e04 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -106,6 +106,7 @@ Lemma Is_true_eq_true2 : (x:bool)  x=true -> (Is_true x).
 Destruct x; Simpl; Auto with bool.
 Save.
 
+(***** TODO
 Lemma eqb_subst : 
   (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2).
 Unfold eqb .
@@ -121,7 +122,8 @@ Intros H.
 Inversion_clear H.
 Trivial with bool.
 Save.
- 
+*****)
+
 Lemma eqb_reflx : (b:bool)(eqb b b)=true.
 Intro b.
 Case b.
-- 
cgit v1.2.3