From 849019c147c7557a9490aaca1942db42f644acbd Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 17 Sep 2009 21:23:35 +0000
Subject: *** empty log message ***

---
 etc/coq/highlighterror.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 etc/coq/highlighterror.v

diff --git a/etc/coq/highlighterror.v b/etc/coq/highlighterror.v
new file mode 100644
index 00000000..26ff1dea
--- /dev/null
+++ b/etc/coq/highlighterror.v
@@ -0,0 +1,9 @@
+(* Test of error highlighting
+
+The error should highlight the last γ₁₂ variable occurrence, the whole
+of it, and only it (not the final dot nor the preceding space).
+*)
+
+Require Import Utf8.
+
+Lemma α₁: ∀ x:nat, ∀ γ₁₂: bool, x = γ₁₂.
-- 
cgit v1.2.3