Rather quick hack to make basic unicode notations available by

requiring a file Utf8_core. That needs to be improved...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13358 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 31 insertions, 13 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index b8e297267..1b92aaf33 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -33,8 +33,6 @@ let dont_load_proofs = ref false
 
 let raw_print = ref false
 
-let unicode_syntax = ref false
-
 (* Compatibility mode *)
 
 type compat_version = V8_2
diff --git a/lib/flags.mli b/lib/flags.mli
index 13cc68a30..1d18b4c51 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -25,8 +25,6 @@ val dont_load_proofs : bool ref
 
 val raw_print : bool ref
 
-val unicode_syntax : bool ref
-
 type compat_version = V8_2
 val compat_version : compat_version option ref
 val version_strictly_greater : compat_version -> bool
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 73f98ca95..6276a23c3 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -409,15 +409,11 @@ let pr_app pr a l =
     pr (lapp,L) a  ++
     prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
-let pr_forall () =
-  if !Flags.unicode_syntax then str"Π" ++ spc ()
-  else str"forall" ++ spc ()
+let pr_forall () = str"forall" ++ spc ()
 
-let pr_fun () =
-  if !Flags.unicode_syntax then str"λ" ++ spc ()
-  else str"fun" ++ spc ()
+let pr_fun () = str"fun" ++ spc ()
 
-let pr_fun_sep = lazy (if !Flags.unicode_syntax then str "," else str " =>")
+let pr_fun_sep = str " =>"
 
 
 let pr_dangling_with_for sep pr inherited a =
@@ -454,7 +450,7 @@ let pr pr sep inherited a =
       hov 0 (
         hov 2 (pr_delimited_binders pr_fun spc
                 (pr mt ltop) bl) ++
-	  Lazy.force pr_fun_sep ++ pr spc ltop a),
+	       pr_fun_sep ++ pr spc ltop a),
       llambda
   | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
       when x=x' ->
diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v
new file mode 100644
index 000000000..a42de3abd
--- /dev/null
+++ b/theories/Unicode/Utf8_core.v
@@ -0,0 +1,25 @@
+(* -*- coding:utf-8 -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Logic *)
+Notation "∀  x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+Notation "∃  x .. y , P" := (exists x, .. (exists y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+
+Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope.
+Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope.
+Notation "x → y" := (x -> y) (at level 90, right associativity): type_scope.
+Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope.
+Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope.
+Notation "x ≠ y" := (x <> y) (at level 70) : type_scope.
+
+(* Abstraction *)
+Notation "'λ'  x .. y , t" := (fun x => .. (fun y => t) ..)
+  (at level 200, x binder, y binder, right associativity).
diff --git a/theories/Unicode/vo.itarget b/theories/Unicode/vo.itarget
index 243a40b76..7be1b9961 100644
--- a/theories/Unicode/vo.itarget
+++ b/theories/Unicode/vo.itarget
@@ -1 +1,2 @@
 Utf8.vo
+Utf8_core.vo
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 29cbde209..b42400662 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -249,7 +249,7 @@ let parse_args arglist =
     | "-emacs-U" :: rem -> Flags.print_emacs := true;
 	Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
 
-    | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
+    | "-unicode" :: rem -> add_require "Utf8_core"; parse rem
 
     | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
     | "-coqlib" :: [] -> usage ()