summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4095.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/4095.v')
-rw-r--r--test-suite/bugs/closed/4095.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
index ffd33d38..8d7dfbd4 100644
--- a/test-suite/bugs/closed/4095.v
+++ b/test-suite/bugs/closed/4095.v
@@ -84,4 +84,4 @@ O1 : T -> PointedOPred
tr : T -> T
O2 : PointedOPred
x0 : T
-H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *) \ No newline at end of file
+H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)