diff options
author | 2008-05-12 12:27:25 +0000 | |
---|---|---|
committer | 2008-05-12 12:27:25 +0000 | |
commit | 7248f6cccfcca2b0d59b244e8789590794aefc45 (patch) | |
tree | 8979753245e2ff2ef183d37ba324f64c90b5d337 /INSTALL.ide | |
parent | bba897d5fd964bef0aa10102ef41cee1ac5fc3bb (diff) |
- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to
change the default pretty-printing to use Π, λ instead of
forall and fun (and allow "," as well as "=>" for "fun" to be more
consistent with the standard forall and exists syntax). Parsing allows
theses new forms too, even if not in -unicode, and does not make Π or
λ keywords. As usual, criticism and suggestions are welcome :)
Not sure what to do about "->"/"→" ?
- [setoid_replace by] now uses tactic3() to get the right parsing level
for tactics.
- Type class [Instance] names are now mandatory.
- Document [rewrite at/by] and fix parsing of occs to support their
combination.
- Backtrack on [Enriching] modifier, now used exclusively in the
implementation of implicit arguments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10921 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'INSTALL.ide')
0 files changed, 0 insertions, 0 deletions