diff options
Diffstat (limited to 'test-suite/bugs/closed/5315.v')
| -rw-r--r-- | test-suite/bugs/closed/5315.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/5315.v b/test-suite/bugs/closed/5315.v index f1f1b8c05..d8824bff8 100644 --- a/test-suite/bugs/closed/5315.v +++ b/test-suite/bugs/closed/5315.v @@ -7,4 +7,4 @@ Function dumb_nope (a:nat) {struct a} := match (id (fun x => x)) a with O => O | S n' => dumb_nope n' end. (* This check is just present to ensure Function worked well *) -Check R_dumb_nope_complete.
\ No newline at end of file +Check R_dumb_nope_complete. |