diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 17:42:32 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 17:42:32 -0400 |
| commit | 30d42837c0ae46aa563761ba20e481f7199d6652 (patch) | |
| tree | 1890e755cf28d8091c0f7f47cc52d5d0c944052d /test-suite/failure | |
| parent | b89502c9f2bf56ee89b7e280815c339ef7b8947c (diff) | |
Add another critical bug to the test-suite.
I have a fix, I'm reviewing it because there may be other bugs around.
Diffstat (limited to 'test-suite/failure')
| -rw-r--r-- | test-suite/failure/cofixpoint.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/failure/cofixpoint.v b/test-suite/failure/cofixpoint.v new file mode 100644 index 000000000..cb39893f4 --- /dev/null +++ b/test-suite/failure/cofixpoint.v @@ -0,0 +1,15 @@ +(* A bug in the guard checking of nested cofixpoints. *) +(* Posted by Maxime Dénès on coqdev (Apr 9, 2014). *) + +CoInductive CoFalse := . + +CoInductive CoTrue := I. + +Fail CoFixpoint loop : CoFalse := + (cofix f := loop with g := loop for f). + +Fail CoFixpoint loop : CoFalse := + (cofix f := I with g := loop for g). + +Fail CoFixpoint loop : CoFalse := + (cofix f := loop with g := I for f).
\ No newline at end of file |