diff options
| author | Pierre-Marie Pédrot | 2020-02-03 18:01:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-03 18:02:39 +0100 |
| commit | a4088339e1948e12f8c0a525577698bc67301a58 (patch) | |
| tree | 5a8421d07cfbcc535644a04f0ddac94330ca4c3a | |
| parent | 1c1c04d0e3e02ce461fb953f08e2d8c68e52ee63 (diff) | |
Test for #5617: Primitive projections confuse the termination checker.
Fixes #5617.
| -rw-r--r-- | test-suite/bugs/closed/bug_5617.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_5617.v b/test-suite/bugs/closed/bug_5617.v new file mode 100644 index 0000000000..c18e79295c --- /dev/null +++ b/test-suite/bugs/closed/bug_5617.v @@ -0,0 +1,8 @@ +Set Primitive Projections. +Record T X := { F : X }. + +Fixpoint f (n : nat) : nat := +match n with +| 0 => 0 +| S m => F _ {| F := f |} m +end. |