diff options
| author | Maxime Dénès | 2014-04-09 17:42:32 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-04-09 17:42:32 -0400 |
| commit | 30d42837c0ae46aa563761ba20e481f7199d6652 (patch) | |
| tree | 1890e755cf28d8091c0f7f47cc52d5d0c944052d | |
| 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.
| -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 0000000000..cb39893f47 --- /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 |