aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5578.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/5578.v')
-rw-r--r--test-suite/bugs/closed/5578.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/5578.v b/test-suite/bugs/closed/5578.v
index 5bcdaa2f1..b9f0bc45c 100644
--- a/test-suite/bugs/closed/5578.v
+++ b/test-suite/bugs/closed/5578.v
@@ -54,4 +54,4 @@ Goal forall (Rat : Set) (PositiveMap_t : Set -> Set)
f eta (
(Bind (k eta) (fun rands =>
ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))).
- (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *) \ No newline at end of file
+ (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)