*** empty log message ***

1 files changed, 9 insertions, 0 deletions

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 = γ₁₂.