diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-05 17:52:38 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-05 17:53:09 +0200 |
| commit | 53b2acb9befe13c0383b923d09a0d5a6c416449e (patch) | |
| tree | f76492f82ac3e1656fa086209b6790f971f47bd1 | |
| parent | 47a2da7326ed975039f9e94780aeb9b1079f4854 (diff) | |
Test file for #5065 - Anomaly: Not a proof by induction
| -rw-r--r-- | test-suite/bugs/closed/5065.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5065.v b/test-suite/bugs/closed/5065.v new file mode 100644 index 000000000..6bd677ba6 --- /dev/null +++ b/test-suite/bugs/closed/5065.v @@ -0,0 +1,6 @@ +Inductive foo := C1 : bar -> foo with bar := C2 : foo -> bar. + +Lemma L1 : foo -> True with L2 : bar -> True. +intros; clear L1 L2; abstract (exact I). +intros; exact I. +Qed.
\ No newline at end of file |