summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3819.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/3819.v')
-rw-r--r--test-suite/bugs/closed/3819.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3819.v b/test-suite/bugs/closed/3819.v
index 355d23a5..0b9c3183 100644
--- a/test-suite/bugs/closed/3819.v
+++ b/test-suite/bugs/closed/3819.v
@@ -6,4 +6,4 @@ Lemma test1 (X:Type) : eq (op OpType X) X.
Proof eq_refl.
Definition test2 (A:Type) : eq (op _ A) A.
-Proof eq_refl. \ No newline at end of file
+Proof eq_refl.