diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_9598.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9598.v b/test-suite/bugs/closed/bug_9598.v index 917bf92a87..daf4d3f847 100644 --- a/test-suite/bugs/closed/bug_9598.v +++ b/test-suite/bugs/closed/bug_9598.v @@ -9,3 +9,15 @@ Module case. Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). End case. + +Module fixpoint. + + Inductive pair := K (n1 : nat) (n2 : nat). + Fixpoint fst (p : pair) : nat := match p with K n _ => n end. + + 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 fixpoint. |