summaryrefslogtreecommitdiff
path: root/tests/coq/misc/NoNestedBorrows.v
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/misc/NoNestedBorrows.v')
-rw-r--r--tests/coq/misc/NoNestedBorrows.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index b044d24f..16a2e816 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -586,4 +586,4 @@ Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 :=
Definition test_shared_borrow_enum2 : result u32 :=
Return 0%u32.
-End NoNestedBorrows .
+End NoNestedBorrows.