From cf136fb80c1b461b16d733830d8a320e6d03d06b Mon Sep 17 00:00:00 2001
From: vsiles
Date: Fri, 5 Oct 2007 13:02:23 +0000
Subject:  Added the automatic generation of the boolean equality if possible
 and the decidability of the usual equality Major changes:  * andb_prop &
 andb_true_intro have been moved from Bool.v to Datatypes.v  * added 2 files: 
    * toplevel/ind_tables.ml* : tables where the boolean eqs and the        
 decidability proofs are stored     * toplevel/auto_ind_decl.ml* : code of the
 schemes that are automatically         generated from inductives types
 (currently boolean eq & decidability )  * improvement of injection: if the
 decidability have been correctly computed,    injection can now break the
 equalities over dependant pair

How to use:
 Set Equality Scheme. to set the automatic generation of the equality when you
create a new inductive type
 Scheme Equality for I. tries to create the equality for the already declared
type I




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

(limited to 'theories/Bool')

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 8f739e0dac..0d674ebf93 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -308,26 +308,12 @@ Hint Resolve orb_comm orb_assoc: bool v62.
 (** * Properties of [andb]     *)
 (*******************************)
 
-Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true.
-Proof.
-  destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
-    auto with bool.
-Qed.
-Hint Resolve andb_prop: bool v62.
-
 Lemma andb_true_eq :
   forall a b:bool, true = a && b -> true = a /\ true = b.
 Proof.
   destruct a; destruct b; auto.
 Defined.
 
-Lemma andb_true_intro :
-  forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true.
-Proof.
-  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
-Qed.
-Hint Resolve andb_true_intro: bool v62.
-
 Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false.
 Proof.
   destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
-- 
cgit v1.2.3