From 7248f6cccfcca2b0d59b244e8789590794aefc45 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 12 May 2008 12:27:25 +0000
Subject: - 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
---
 lib/flags.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 60d6c7836f..36179bc8ab 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
-- 
cgit v1.2.3