- 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



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

6 files changed, 45 insertions, 27 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 69726e9cb..aea5c5628 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -204,7 +204,7 @@ doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex
 
 # Not robust, improve...
 ide/index_urls.txt: doc/refman/html/index.html
-	- rm ide/index_url.txt
+	- rm ide/index_urls.txt
 	cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-itemize | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt
 
 
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 6649dc31a..44de2f358 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -26,7 +26,7 @@
       [  "Add" ; "Check"; "Eval"; "Extraction" ;
 	 "Load" ; "Undo";
 	 "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ;
-	 "End" ; "Section"
+	 "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments"
       ];
     Hashtbl.mem h
 
@@ -48,14 +48,14 @@
 	  "Proposition" ; "Property" ;
           (* Definitions *)
 	  "Definition" ; "Let" ; "Example" ; "SubClass" ;
-          "Fixpoint" ; "CoFixpoint"; 
+          "Fixpoint" ; "CoFixpoint" ; "Scheme" ;
           (* Assumptions *)
 	  "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
 	  "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters";
           (* Inductive *)
           "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
           (* Other *)
-	  "Ltac" ; "Typeclasses"; "Instance"
+	  "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class"
 	];
       Hashtbl.mem h
 
@@ -73,6 +73,8 @@ let ident = firstchar identchar*
 let multiword_declaration =
   "Module" (space+ "Type")
 | "Program" space+ ident
+| "Existing" space+ "Instance"
+| "Canonical" space+ "Structure"
 
 let locality = ("Local" space+)?
 
@@ -80,14 +82,25 @@ let multiword_command =
   "Set" (space+ ident)* 
 | "Unset" (space+ ident)* 
 | "Open" space+ locality "Scope"
+| "Close" space+ locality "Scope"
+| "Bind" space+ "Scope"
+| "Arguments" space+ "Scope"
+| "Reserved" space+ "Notation" space+ locality
+| "Delimit" space+ "Scope"
 | "Next" space+ "Obligation"
 | "Solve" space+ "Obligations"
-| "Require" space+ ("Import"|"Export")
+| "Require" space+ ("Import"|"Exportp")
 | "Infix" space+ locality
 | "Notation" space+ locality
 | "Hint" space+ locality ident
 | "Reset" (space+ "Initial")?
 | "Tactic" space+ "Notation"
+| "Implicit" space+ "Arguments"
+| "Implicit" space+ ("Type"|"Types")
+| "Combined" space+ "Scheme"
+
+(* At least still missing: "Inline" + decl, variants of "Identity
+  Coercion", variants of Print, Add, ... *)
 
 rule next_starting_order = parse
   | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ddaba47b0..3769d7b3e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -824,7 +824,7 @@ GEXTEND Gram
     [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
   ;
   locality:
-    [ [ IDENT "Local" -> true | -> false ] ]
+    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> false ] ]
   ;
   non_globality:
     [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ]
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 96e01a731..1df0a7833 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id:$ i*)
 
 Require Import ZTimesOrder.
 Require Import ZArith.
@@ -246,4 +246,4 @@ case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H;
 [reflexivity | discriminate H | discriminate H].
 now apply Zcompare_Eq_eq.
 Qed.
-*)
\ No newline at end of file
+*)
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.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 46faafb23..610afd4d7 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -80,7 +80,8 @@ Close Local Scope positive_scope.
 Definition Zplus (x y:Z) :=
   match x, y with
     | Z0, y => y
-    | x, Z0 => x
+    | Zpos x', Z0 => Zpos x'
+    | Zneg x', Z0 => Zneg x'
     | Zpos x', Zpos y' => Zpos (x' + y')
     | Zpos x', Zneg y' =>
       match (x' ?= y')%positive Eq with