From b6c6e36afa8da16a62bf16191baa2531894c54fc Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 11 May 2008 20:42:52 +0000 Subject: - Changement du code de Zplus pour accomoder ring qui sinon prend une complexité exponentielle dans la machine lazy depuis que l'algo de compilation du filtrage évite systématiquement d'expanser quand le filtrage n'est pas dépendant. - Un peu plus de colorisation dans coqide. - Utilisation de formats pour améliorer de l'affichage des notations Utf8. - Systématisation paire Local/Global dans g_vernac.ml4 (même si le défaut n'est pas toujours le même) - Bug Makefile MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10918 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Unicode/Utf8.v | 40 ++++++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 18 deletions(-) (limited to 'theories/Unicode') diff --git a/theories/Unicode/Utf8.v b/theories/Unicode/Utf8.v index 0a0a3b95d..32b892b63 100644 --- a/theories/Unicode/Utf8.v +++ b/theories/Unicode/Utf8.v @@ -8,25 +8,29 @@ (************************************************************************) (* Logic *) -Notation "∀ x , P" := - (forall x , P) (at level 200, x ident) : type_scope. -Notation "∀ x y , P" := - (forall x y , P) (at level 200, x ident, y ident) : type_scope. -Notation "∀ x y z , P" := - (forall x y z , P) (at level 200, x ident, y ident, z ident) : type_scope. -Notation "∀ x y z u , P" := - (forall x y z u , P) (at level 200, x ident, y ident, z ident, u ident) : type_scope. -Notation "∀ x : t , P" := - (forall x : t , P) (at level 200, x ident) : type_scope. -Notation "∀ x y : t , P" := - (forall x y : t , P) (at level 200, x ident, y ident) : type_scope. -Notation "∀ x y z : t , P" := - (forall x y z : t , P) (at level 200, x ident, y ident, z ident) : type_scope. -Notation "∀ x y z u : t , P" := - (forall x y z u : t , P) (at level 200, x ident, y ident, z ident, u ident) : type_scope. +Notation "∀ x , P" := (forall x , P) + (at level 200, x ident, right associativity) : type_scope. +Notation "∀ x y , P" := (forall x y , P) + (at level 200, x ident, y ident, right associativity) : type_scope. +Notation "∀ x y z , P" := (forall x y z , P) + (at level 200, x ident, y ident, z ident, right associativity) : type_scope. +Notation "∀ x y z u , P" := (forall x y z u , P) + (at level 200, x ident, y ident, z ident, u ident, right associativity) + : type_scope. +Notation "∀ x : t , P" := (forall x : t , P) + (at level 200, x ident, right associativity) : type_scope. +Notation "∀ x y : t , P" := (forall x y : t , P) + (at level 200, x ident, y ident, right associativity) : type_scope. +Notation "∀ x y z : t , P" := (forall x y z : t , P) + (at level 200, x ident, y ident, z ident, right associativity) : type_scope. +Notation "∀ x y z u : t , P" := (forall x y z u : t , P) + (at level 200, x ident, y ident, z ident, u ident, right associativity) + : type_scope. -Notation "∃ x , P" := (exists x , P) (at level 200, x ident) : type_scope. -Notation "∃ x : t , P" := (exists x : t, P) (at level 200, x ident) : type_scope. +Notation "∃ x , P" := (exists x , P) + (at level 200, x ident, right associativity) : type_scope. +Notation "∃ x : t , P" := (exists x : t, P) + (at level 200, x ident, 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. -- cgit v1.2.3