diff options
| author | Gaëtan Gilbert | 2020-02-04 13:24:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-04 13:24:19 +0100 |
| commit | d07b2862ec9a562f72c2f85e1b5f4529de200a07 (patch) | |
| tree | 76a521b90f36fbc7676a9cce7d4135252bff140d | |
| parent | c14ce309cee3d5dea706edd8c54b0556111fffc0 (diff) | |
| parent | a4088339e1948e12f8c0a525577698bc67301a58 (diff) | |
Merge PR #11513: Test for #5617: Primitive projections confuse the termination checker.
Reviewed-by: SkySkimmer
| -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. |