diff options
| author | Jasper Hugunin | 2020-12-15 20:47:27 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2020-12-15 20:47:27 -0800 |
| commit | 7f6883f9a5a6593e667ba4e21fdeccda5c80c589 (patch) | |
| tree | bf1fe802381527f825718e3c41fa32a721976db4 | |
| parent | 303b167ff91e014768ee0286bf8dc0e202778b56 (diff) | |
Modify Bool/IfProp.v to compile with -mangle-names
| -rw-r--r-- | theories/Bool/IfProp.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 7e9087c377..8366e8257e 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -29,13 +29,13 @@ case diff_true_false; trivial with bool. Qed. Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A. -intros. +intros A B H. inversion H. assumption. Qed. Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B. -intros. +intros A B H. inversion H. assumption. Qed. @@ -45,7 +45,7 @@ destruct 1; auto with bool. Qed. Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. -destruct b; intro H. +intros A B b; destruct b; intro H. - left; inversion H; auto with bool. - right; inversion H; auto with bool. Qed. |