aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/interactive
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/interactive')
-rw-r--r--test-suite/interactive/ParalITP.v2
-rw-r--r--test-suite/interactive/proof_block.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/interactive/ParalITP.v b/test-suite/interactive/ParalITP.v
index a96d4a5c7..7fab2a58e 100644
--- a/test-suite/interactive/ParalITP.v
+++ b/test-suite/interactive/ParalITP.v
@@ -44,4 +44,4 @@ split.
exact a.
Qed.
-End Demo. \ No newline at end of file
+End Demo.
diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
index 31e349376..a865632e8 100644
--- a/test-suite/interactive/proof_block.v
+++ b/test-suite/interactive/proof_block.v
@@ -63,4 +63,4 @@ split. split. split.
- solve [ trivial ].
- solve [ trivial ].
- exact 6.
-Qed. \ No newline at end of file
+Qed.