aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2008-06-06 08:19:00 +0000
committerPierre Courtieu2008-06-06 08:19:00 +0000
commitfaea8019ff496be6b5bf49f8257117fb1bddacef (patch)
tree3f8982776e7468d7c65831ac69b8267f232569cc
parent5e0a938a7b3558dd5de94f6cb52cbebf8379014e (diff)
Fixed example file for utf8.
-rw-r--r--coq/utf8.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/utf8.v b/coq/utf8.v
index ab702dcb..ad02b2c2 100644
--- a/coq/utf8.v
+++ b/coq/utf8.v
@@ -50,7 +50,7 @@ Notation "x ≥ y" := (ge x y) (at level 70, no associativity).
(* test *)
(*
-Goal ∀ x, True -> (∃ y , x ≥ y + 1) ∨ x ≤ y.
+Goal ∀ x, True -> (∃ y , x ≥ y + 1) ∨ x ≤ 0.
*)
(* Test for error message