- 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

2 files changed, 4 insertions, 0 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 60d6c7836..36179bc8a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -32,6 +32,8 @@ let dont_load_proofs = ref false
 
 let raw_print = ref false
 
+let unicode_syntax = ref false
+
 (* Translate *)
 let translate = ref false
 let make_translate f = translate := f
diff --git a/lib/flags.mli b/lib/flags.mli
index c14e223e7..2301d8a0d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -27,6 +27,8 @@ val dont_load_proofs : bool ref
 
 val raw_print : bool ref
 
+val unicode_syntax : bool ref
+
 val translate : bool ref
 val make_translate : bool -> unit
 val do_translate : unit -> bool