diff options
| author | Xavier Clerc | 2014-11-14 16:32:07 +0100 |
|---|---|---|
| committer | Xavier Clerc | 2014-11-14 16:32:07 +0100 |
| commit | 54a67aeb7955687ad67c958a5d4de9e21164e8db (patch) | |
| tree | af093664ba14301d5eadef6762b15535093bcdeb | |
| parent | f43c3bc3165567173c86d5f425fb834018c22a1b (diff) | |
Add missing "Fail" to test case for bug #2814.
| -rw-r--r-- | test-suite/bugs/opened/2814.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/2814.v b/test-suite/bugs/opened/2814.v index d8f6b906a1..a740b4384d 100644 --- a/test-suite/bugs/opened/2814.v +++ b/test-suite/bugs/opened/2814.v @@ -2,4 +2,4 @@ Require Import Program. Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False. intros. - induction H. + Fail induction H. |