summaryrefslogtreecommitdiff
path: root/tests/coq/misc/Paper.v
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/Paper.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 4a49096f..6b110193 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -128,4 +128,4 @@ Definition call_choose (p : (u32 * u32)) : result u32 :=
Return px0
.
-End Paper .
+End Paper.