diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-07 19:21:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:59 +0200 |
| commit | 4cb7fe525a472928aee02d772458d28a2b71072a (patch) | |
| tree | 5934260488727e9c06871ce775376535c252f721 /test-suite | |
| parent | 2d6de8b102ea3cd05c5d193190faf787ccb84baa (diff) | |
- 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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/unicode_utf8.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v index bfddd8468..50a65310d 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. |