From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- test-suite/bugs/closed/4132.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/bugs/closed/4132.v') diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v index 806ffb77..67ecc308 100644 --- a/test-suite/bugs/closed/4132.v +++ b/test-suite/bugs/closed/4132.v @@ -26,6 +26,6 @@ Qed. Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. omega. (* Pierre L: according to a comment of bug report #4132, - this might have triggered "Failure(occurence 2)" in the past, + this might have triggered "Failure(occurrence 2)" in the past, but I never managed to reproduce that. *) Qed. -- cgit v1.2.3