aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/cbn.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/cbn.v')
-rw-r--r--test-suite/success/cbn.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v
index 6aeb05f54..c98689c23 100644
--- a/test-suite/success/cbn.v
+++ b/test-suite/success/cbn.v
@@ -15,4 +15,4 @@ Goal forall n, foo (S n) = g n.
match goal with
|- g _ = g _ => reflexivity
end.
-Qed. \ No newline at end of file
+Qed.