diff options
Diffstat (limited to 'test-suite/bugs/closed/5618.v')
| -rw-r--r-- | test-suite/bugs/closed/5618.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v index ab88a88f4..47e0e92d2 100644 --- a/test-suite/bugs/closed/5618.v +++ b/test-suite/bugs/closed/5618.v @@ -6,4 +6,4 @@ Function test {T} (v : T) (x : nat) : nat := | S x' => test v x' end. -Check R_test_complete.
\ No newline at end of file +Check R_test_complete. |