diff options
Diffstat (limited to 'test-suite/bugs/closed/4250.v')
| -rw-r--r-- | test-suite/bugs/closed/4250.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4250.v b/test-suite/bugs/closed/4250.v index 74cacf559..f5d0d1a52 100644 --- a/test-suite/bugs/closed/4250.v +++ b/test-suite/bugs/closed/4250.v @@ -8,4 +8,4 @@ Function f2 {A:Type} {n:nat} {v:Vector.t A n} : nat := n. (* fails with "The reference A was not found in the current environment." *) Function f3 `{n:nat , u:Vector.t A n} := u. -Check R_f3_complete.
\ No newline at end of file +Check R_f3_complete. |