summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4498.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/4498.v')
-rw-r--r--test-suite/bugs/closed/4498.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v
index ccdb2ddd..379e46b3 100644
--- a/test-suite/bugs/closed/4498.v
+++ b/test-suite/bugs/closed/4498.v
@@ -21,4 +21,4 @@ Require Export Coq.Setoids.Setoid.
Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
signature equiv ==> equiv ==> equiv as compose_mor.
-Proof. apply comp_respects. Qed. \ No newline at end of file
+Proof. apply comp_respects. Qed.