diff options
| author | Pierre-Marie Pédrot | 2015-11-30 12:36:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-30 12:36:04 +0100 |
| commit | 30efd8d3501ff724e6f75acf7c2355a107da1c70 (patch) | |
| tree | 03ab3b3f2d78b30e8b762f21c1c84e4e341e61d0 | |
| parent | 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 (diff) | |
Test for bug #4149.
| -rw-r--r-- | test-suite/bugs/closed/4149.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4149.v b/test-suite/bugs/closed/4149.v new file mode 100644 index 0000000000..b81c680cd7 --- /dev/null +++ b/test-suite/bugs/closed/4149.v @@ -0,0 +1,4 @@ +Goal forall A, A -> Type. +Proof. + intros; eauto. +Qed. |