diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_9598.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9598.v b/test-suite/bugs/closed/bug_9598.v index daf4d3f847..00bbfcf5d9 100644 --- a/test-suite/bugs/closed/bug_9598.v +++ b/test-suite/bugs/closed/bug_9598.v @@ -21,3 +21,16 @@ Module fixpoint. Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). End fixpoint. + +Module primproj. + + Set Primitive Projections. + + Inductive pair := K { fst : nat; snd : nat }. + + Definition alias_K a b := K a b. + + Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)). + Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). + +End primproj. |