From 4cb7fe525a472928aee02d772458d28a2b71072a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 19:21:05 +0200
Subject: - Fix arity handling in retyping (de Bruijn bug!) - Enforce that no u
 <= Prop/Set can be added for u introduced by the user in
 Evd.process_constraints. (Needs to be enforced in the kernel as well, but
 that's the main entry point). - Fix a test-suite script and remove a
 regression comment, it's just as before now.

---
 test-suite/success/unicode_utf8.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v
index bfddd84682..50a65310d1 100644
--- a/test-suite/success/unicode_utf8.v
+++ b/test-suite/success/unicode_utf8.v
@@ -11,7 +11,7 @@ Parameter π : ℝ.
 
 (** Check indices *)
 Definition test_indices : nat -> nat := fun x₁ => x₁.
-Definition π₂ := snd.
+Definition π₂ := @snd.
 
 (** More unicode in identifiers *)
 Definition αβ_áà_אב := 0.
-- 
cgit v1.2.3