diff options
| author | Jasper Hugunin | 2020-08-24 12:25:39 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:31 -0700 |
| commit | afdfbcfcb2156b22527df1d8d019f6f667145689 (patch) | |
| tree | 07778960b9f3ed57e0dcebbadbd1573fc9b7798d | |
| parent | 20b6715c5172a4483c52b743ead2ed53eb82e7d6 (diff) | |
Modify Bool/Bool.v to compile with -mangle-names
| -rw-r--r-- | theories/Bool/Bool.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 9e10786fcd..0f62db42cf 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -258,7 +258,7 @@ Qed. Lemma orb_true_elim : forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}. Proof. - destruct b1; simpl; auto. + intro b1; destruct b1; simpl; auto. Defined. Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true. @@ -424,7 +424,7 @@ Notation andb_true_b := andb_true_l (only parsing). Lemma andb_false_elim : forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}. Proof. - destruct b1; simpl; auto. + intro b1; destruct b1; simpl; auto. Defined. Hint Resolve andb_false_elim: bool. @@ -681,17 +681,17 @@ Qed. Lemma negb_xorb_l : forall b b', negb (xorb b b') = xorb (negb b) b'. Proof. - destruct b,b'; trivial. + intros b b'; destruct b,b'; trivial. Qed. Lemma negb_xorb_r : forall b b', negb (xorb b b') = xorb b (negb b'). Proof. - destruct b,b'; trivial. + intros b b'; destruct b,b'; trivial. Qed. Lemma xorb_negb_negb : forall b b', xorb (negb b) (negb b') = xorb b b'. Proof. - destruct b,b'; trivial. + intros b b'; destruct b,b'; trivial. Qed. (** Lemmas about the [b = true] embedding of [bool] to [Prop] *) |