diff options
| author | herbelin | 2010-07-30 08:46:55 +0000 |
|---|---|---|
| committer | herbelin | 2010-07-30 08:46:55 +0000 |
| commit | 866394da512c3bac91a703c038e6a4781811629e (patch) | |
| tree | d05c1b32d8bf1b66451623834e782989d91d4ebd /plugins/pluginsopt.itarget | |
| parent | 0bd0b1d55aba3f0ca0f495377b9aca8ef4fc4163 (diff) | |
r13359 continued: removed native treatment for λ (lambda) and Π (Pi)
what frees the tokens for other uses in non-unicode mode.
For Π, users will have to introduce their own recursive notation.
For λ, this is provided by the -unicode option (which actually is not
documented nor as an option nor in the reference manual; maybe it
should simply be now removed since "Require Import Utf8_core" has the
same effect).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13359 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/pluginsopt.itarget')
0 files changed, 0 insertions, 0 deletions