diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-10 12:58:01 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-10 12:58:01 +0000 |
commit | fb1e00c4581221aff6787debe885b87c386600f3 (patch) | |
tree | 42823cfab1d22eaaeb46e8e7e6f813ccf69b7b86 /test-suite/success/unicode_utf8.v | |
parent | 3b03eb1015f14e04e505b11c27fb38b7db6ebe87 (diff) |
Centralisation de la détection lettre/symbole par le lexeur dans les plages unicode; ajout de nouvelles plages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8800 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/unicode_utf8.v')
-rw-r--r-- | test-suite/success/unicode_utf8.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v index e3c4dd300..19e306fea 100644 --- a/test-suite/success/unicode_utf8.v +++ b/test-suite/success/unicode_utf8.v @@ -4,6 +4,9 @@ (* Check Greek letters *) Definition test_greek : nat -> nat := fun Δ => Δ. +Parameter ℝ : Set. +Parameter π : ℝ. (* Check indices *) Definition test_indices : nat -> nat := fun x₁ => x₁. +Definition π₂ := snd. |