diff options
| -rw-r--r-- | Makefile.doc | 2 | ||||
| -rw-r--r-- | ide/highlight.mll | 21 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 4 | ||||
| -rw-r--r-- | theories/Unicode/Utf8.v | 40 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 3 |
6 files changed, 45 insertions, 27 deletions
diff --git a/Makefile.doc b/Makefile.doc index 69726e9cb8..aea5c5628d 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 6649dc31a7..44de2f3581 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 ddaba47b0b..3769d7b3e6 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 96e01a731c..1df0a78339 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 0a0a3b95db..32b892b639 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 46faafb23c..610afd4d7d 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 |