From 58c70113a815a42593c566f64f2de840fc7e48a1 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 4 Mar 2008 17:33:35 +0000 Subject: migration from Set to Type of FSet/FMap + some dependencies... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 652ac955e..686118e4b 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -196,7 +196,7 @@ Qed. Lemma if_negb : - forall (A:Set) (b:bool) (x y:A), + forall (A:Type) (b:bool) (x y:A), (if negb b then x else y) = (if b then y else x). Proof. destruct b; trivial. @@ -686,14 +686,14 @@ Qed. (* Rewrite rules about andb, orb and if (used in romega) *) -Lemma andb_if : forall (A:Set)(a a':A)(b b' : bool), +Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool), (if b && b' then a else a') = (if b then if b' then a else a' else a'). Proof. destruct b; destruct b'; auto. Qed. -Lemma negb_if : forall (A:Set)(a a':A)(b:bool), +Lemma negb_if : forall (A:Type)(a a':A)(b:bool), (if negb b then a else a') = (if b then a' else a). Proof. -- cgit v1.2.3