diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_9598.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9598.v b/test-suite/bugs/closed/bug_9598.v new file mode 100644 index 0000000000..917bf92a87 --- /dev/null +++ b/test-suite/bugs/closed/bug_9598.v @@ -0,0 +1,11 @@ +Module case. + + Inductive pair := K (n1 : nat) (n2 : nat). + Definition 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 case. |