aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/coercions.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/coercions.v')
-rw-r--r--test-suite/success/coercions.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index b538d2ed2..9b11bc011 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -130,4 +130,4 @@ Local Coercion l2v2 : list >-> vect.
of coercions *)
Fail Check (fun l : list (T1 * T1) => (l : vect _ _)).
Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)).
-Section what_we_could_do. \ No newline at end of file
+Section what_we_could_do.