aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3943.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/3943.v')
-rw-r--r--test-suite/bugs/closed/3943.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3943.v b/test-suite/bugs/closed/3943.v
index 5e5ba816f..ac9c50369 100644
--- a/test-suite/bugs/closed/3943.v
+++ b/test-suite/bugs/closed/3943.v
@@ -47,4 +47,4 @@ Definition path_isomorphic (i j : Isomorphic s d)
Admitted.
Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q
-: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q. \ No newline at end of file
+: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.