diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1446.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1446.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v index d4e7cea8..8cb2d653 100644 --- a/test-suite/bugs/closed/shouldsucceed/1446.v +++ b/test-suite/bugs/closed/shouldsucceed/1446.v @@ -1,8 +1,8 @@ Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false. Proof. - destruct b;intros;trivial. - elim H. - exact (refl_equal true). + destruct b;intros;trivial. + elim H. + exact (refl_equal true). Qed. Section BUG. @@ -13,7 +13,7 @@ Section BUG. Hypothesis H1 : b <> true. Goal False. - rewrite (not_true_eq_false _ H) in * |-. + rewrite (not_true_eq_false _ H) in * |-. contradiction. Qed. |