Concentration des notations officielles dans Init/Notations; restructuration de Init

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

11 files changed, 254 insertions, 144 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index a012d4e36..c0c999c4c 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -8,6 +8,8 @@
 
 (*i $Id$ i*)
 
+Require Notations.
+
 Set Implicit Arguments.
 V7only [Unset Implicit Arguments.].
 
@@ -52,7 +54,7 @@ Inductive sum [A,B:Set] : Set
     := inl : A -> (sum A B)
      | inr : B -> (sum A B).
 
-Infix "+" sum (at level 4, left associativity) : type_scope.
+Notation "x + y" := (sum x y) : type_scope.
 Arguments Scope sum [type_scope type_scope].
 
 (** [prod A B], written [A * B], is the product of [A] and [B];
@@ -63,11 +65,8 @@ Add Printing Let prod.
 
 Arguments Scope prod [type_scope type_scope].
 
-Notation "x * y" := (prod x y) (at level 3, right associativity) : type_scope
-  V8only (at level 30, left associativity).
-
-Notation "( x , y )" := (pair ? ? x y) (at level 0)
-  V8only "x , y" (at level 150, left associativity).
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y )" := (pair ? ? x y) V8only "x , y".
 
 Section projections.
    Variables A,B:Set.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index aace0f804..91ec84c42 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -11,6 +11,7 @@
 Set Implicit Arguments.
 V7only [Unset Implicit Arguments.].
 
+Require Notations.
 Require Datatypes.
 
 (** [True] is the always true proposition *)
@@ -22,8 +23,16 @@ Inductive False : Prop := .
 (** [not A], written [~A], is the negation of [A] *)
 Definition not := [A:Prop]A->False.
 
+Notation "~ x" := (not x).
+
 Hints Unfold not : core.
 
+Inductive and [A,B:Prop] : Prop as "A /\ B" := conj : A -> B -> A /\ B.
+
+V7only[
+Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1).
+].
+
 Section Conjunction.
 
   (** [and A B], written [A /\ B], is the conjunction of [A] and [B]
@@ -33,52 +42,47 @@ Section Conjunction.
 
       [proj1] and [proj2] are first and second projections of a conjunction *)
 
-  Inductive and [A,B:Prop] : Prop := conj : A -> B -> (and A B).
-
   Variables A,B : Prop.
 
   Theorem proj1 : (and A B) -> A.
   Proof.
-  Induction 1; Trivial.
+  NewDestruct 1; Trivial.
   Qed.
 
   Theorem proj2 : (and A B) -> B.
   Proof.
-  Induction 1; Trivial.
+  NewDestruct 1; Trivial.
   Qed.
 
 End Conjunction.
 
-Section Disjunction.
-
-  (** [or A B], written [A \/ B], is the disjunction of [A] and [B] *)
+(** [or A B], written [A \/ B], is the disjunction of [A] and [B] *)
 
-  Inductive or [A,B:Prop] : Prop :=
-       or_introl : A -> (or A B) 
-     | or_intror : B -> (or A B).
+Inductive or [A,B:Prop] : Prop as "A \/ B":=
+     or_introl : A -> A \/ B 
+   | or_intror : B -> A \/ B.
 
-End Disjunction.
+(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
 
-Section Equivalence.
-
-  (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
+Definition iff := [A,B:Prop] (and (A->B) (B->A)).
 
-  Definition iff := [P,Q:Prop] (and (P->Q) (Q->P)).
+Notation "A <-> B" := (iff A B).
 
+Section Equivalence.
 
-Theorem iff_refl : (a:Prop) (iff a a).
+Theorem iff_refl : (A:Prop) (iff A A).
   Proof.
     Split; Auto.
   Qed.
 
-Theorem iff_trans : (a,b,c:Prop) (iff a b) -> (iff b c) -> (iff a c).
+Theorem iff_trans : (A,B,C:Prop) (iff A B) -> (iff B C) -> (iff A C).
   Proof.
-    Intros a b c (H1,H2) (H3,H4); Split; Auto.
+    Intros A B C (H1,H2) (H3,H4); Split; Auto.
   Qed.
 
-Theorem iff_sym : (a,b:Prop) (iff a b) -> (iff b a).
+Theorem iff_sym : (A,B:Prop) (iff A B) -> (iff B A).
   Proof.
-    Intros a b (H1,H2); Split; Auto.
+    Intros A B (H1,H2); Split; Auto.
   Qed.
 
 End Equivalence.
@@ -87,6 +91,10 @@ End Equivalence.
     denotes either [P] and [Q], or [~P] and [Q] *)
 Definition IF := [P,Q,R:Prop] (or (and P Q) (and (not P) R)).
 
+Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3)
+  (at level 1, c1, c2, c3 at level 8)
+  V8only (at level 200).
+
 Section First_order_quantifiers.
 
   (** [(ex A P)], or simply [(EX x | P(x))], expresses the existence of an 
@@ -110,20 +118,37 @@ Section First_order_quantifiers.
 
   Definition all := [A:Type][P:A->Prop](x:A)(P x). 
 
-End First_order_quantifiers.
+  Section universal_quantification.
 
-Section Equality.
+  Variable A : Type.
+  Variable P : A->Prop.
 
-  (** [(eq A x y)], or simply [x=y], expresses the (Leibniz') equality
-      of [x] and [y]. Both [x] and [y] must belong to the same type [A].
-      The definition is inductive and states the reflexivity of the equality.
-      The others properties (symmetry, transitivity, replacement of 
-      equals) are proved below *)
+  Theorem inst : (x:A)(all ? [x](P x))->(P x).
+  Proof.
+  Unfold all; Auto.
+  Qed.
+
+  Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(all A P).
+  Proof.
+  Red; Auto.
+  Qed.
 
-  Inductive eq [A:Type;x:A] : A->Prop
-         := refl_equal : (eq A x x).
+  End universal_quantification.
 
-End Equality.
+End First_order_quantifiers.
+
+(** [(eq A x y)], or simply [x=y], expresses the (Leibniz') equality
+    of [x] and [y]. Both [x] and [y] must belong to the same type [A].
+    The definition is inductive and states the reflexivity of the equality.
+    The others properties (symmetry, transitivity, replacement of 
+    equals) are proved below *)
+
+Inductive eq [A:Type;x:A] : (y:A)Prop as "x = y :> A"
+       := refl_equal : x = x :> A.
+
+Notation "x = y" := (eq ? x y).
+Notation "x <> y  :> T" := ~ (!eq T x y).
+Notation "x <> y" := ~ x=y.
 
 Hints Resolve I conj or_introl or_intror refl_equal : core v62.
 Hints Resolve ex_intro ex_intro2 : core v62.
@@ -133,7 +158,7 @@ Section Logic_lemmas.
   Theorem absurd : (A:Prop)(C:Prop) A -> (not A) -> C.
   Proof.
     Unfold not; Intros A C h1 h2.
-    Elim (h2 h1).
+    NewDestruct (h2 h1).
   Qed.
 
   Section equality.
@@ -142,26 +167,26 @@ Section Logic_lemmas.
     Variable x,y,z : A.
 
     Theorem sym_eq : (eq ? x y) -> (eq ? y x).
-      Proof.
-     Induction 1; Trivial.
+    Proof.
+     NewDestruct 1; Trivial.
     Defined.
     Opaque sym_eq.
 
     Theorem trans_eq : (eq ? x y) -> (eq ? y z) -> (eq ? x z).
     Proof.
-     Induction 2; Trivial.
+     NewDestruct 2; Trivial.
     Defined.
     Opaque trans_eq.
 
     Theorem f_equal : (eq ? x y) -> (eq ? (f x) (f y)).
     Proof.
-     Induction 1; Trivial.
+     NewDestruct 1; Trivial.
     Defined.
     Opaque f_equal.
 
     Theorem sym_not_eq : (not (eq ? x y)) -> (not (eq ? y x)).
     Proof.
-     Red; Intros h1 h2; Apply h1; Case h2; Trivial.
+     Red; Intros h1 h2; Apply h1; NewDestruct h2; Trivial.
     Qed.
 
     Definition sym_equal     := sym_eq.
@@ -176,34 +201,34 @@ Section Logic_lemmas.
    Intros.
    Cut (identity A x y).
    NewDestruct 1; Auto.
-   Elim H; Auto.
+   NewDestruct H; Auto.
   Qed.
 *)
 
   Definition eq_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eq ? y x)->(P y).
-   Intros A x P H y H0; Elim sym_eq with 1:= H0; Trivial.
+   Intros A x P H y H0; Elim sym_eq with 1:= H0; Assumption.
   Defined.
 
   Definition eq_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)(eq ? y x)->(P y).
-    Intros A x P H y H0; Elim sym_eq with 1:= H0; Trivial.
+    Intros A x P H y H0; Elim sym_eq with 1:= H0; Assumption.
   Defined.
 
   Definition eq_rect_r : (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? y x)->(P y).
-    Intros A x P H y H0; Elim sym_eq with 1:= H0; Trivial.
+    Intros A x P H y H0; Elim sym_eq with 1:= H0; Assumption.
   Defined.
 End Logic_lemmas.
 
 Theorem f_equal2 : (A1,A2,B:Type)(f:A1->A2->B)(x1,y1:A1)(x2,y2:A2)
   (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? (f x1 x2) (f y1 y2)).
 Proof.
-  Induction 1; Induction 1; Trivial.
+  NewDestruct 1; NewDestruct 1; Reflexivity.
 Qed.
 
 Theorem f_equal3 : (A1,A2,A3,B:Type)(f:A1->A2->A3->B)(x1,y1:A1)(x2,y2:A2)
   (x3,y3:A3)(eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) 
    -> (eq ? (f x1 x2 x3) (f y1 y2 y3)).
 Proof.
-  Induction 1; Induction 1; Induction 1; Trivial.
+  NewDestruct 1; NewDestruct 1; NewDestruct 1; Reflexivity.
 Qed.
 
 Theorem f_equal4 : (A1,A2,A3,A4,B:Type)(f:A1->A2->A3->A4->B)
@@ -211,7 +236,7 @@ Theorem f_equal4 : (A1,A2,A3,A4,B:Type)(f:A1->A2->A3->A4->B)
   (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4)
    -> (eq ? (f x1 x2 x3 x4) (f y1 y2 y3 y4)).
 Proof.
-  Induction 1; Induction 1; Induction 1; Induction 1; Trivial.
+  NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1; Reflexivity.
 Qed.
 
 Theorem f_equal5 : (A1,A2,A3,A4,A5,B:Type)(f:A1->A2->A3->A4->A5->B)
@@ -219,7 +244,8 @@ Theorem f_equal5 : (A1,A2,A3,A4,A5,B:Type)(f:A1->A2->A3->A4->A5->B)
   (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4) -> (eq ? x5 y5)
     -> (eq ? (f x1 x2 x3 x4 x5) (f y1 y2 y3 y4 y5)).
 Proof.
-  Induction 1; Induction 1; Induction 1; Induction 1; Induction 1; Trivial.
+  NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1;
+  Reflexivity.
 Qed.
 
 Hints Immediate sym_eq sym_not_eq : core v62.
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 483221be2..a16583dd4 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -8,16 +8,18 @@
 
 (*i $Id$ i*)
 
+Require Export Notations.
 Require Export Logic.
 
 (** Symbolic notations for things in [Logic.v] *)
+(*
 V7only[
 Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1).
 ].
 
 Notation "~ x" := (not x) (at level 5, right associativity)
   V8only (at level 55, right associativity).
-Notation "x = y  :> T" := (!eq T x y) (at level 5, y at next level, no associativity).
+Notation "x = y  :> T" := (!eq T x y).
 Notation "x = y" := (eq ? x y) (at level 5, no associativity).
 Notation "x <> y  :> T" := (not (!eq T x y)) (at level 5, y at next level, no associativity).
 Notation "x <> y" := (not (eq ? x y)) (at level 5, no associativity).
@@ -29,6 +31,7 @@ Infix RIGHTA 8 "<->" iff.
 Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3)
   (at level 1, c1, c2, c3 at level 8)
   V8only (at level 200).
+*)
 
 (* Order is important to give printing priority to fully typed ALL and EX *)
 
@@ -52,10 +55,12 @@ Notation "'EX' x : t | p & q"   := (ex2 t [x:t]p [x:t]q)
   (at level 10, p, q at level 8)
   V8only "'EX2' x : t | p & q" (at level 200, x at level 80).
 
+V7only[
 (** Parsing only of things in [Logic.v] *)
 
-V7only[
 Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing).
 Notation "< A > x = y" := (eq A x y)
   (A annot, at level 1, x at level 0, only parsing).
+Notation "< A > x <> y" := ~(eq A x y)
+  (A annot, at level 1, x at level 0, only parsing).
 ].
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 5ad3716ed..bdb3f687c 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -18,17 +18,20 @@ Require Export Logic.
 Require LogicSyntax.
 
 
+(*
 (** [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)]
    when [A] is of type [Type] *)
 
-(*
 Definition allT := [A:Type][P:A->Prop](x:A)(P x). 
 *)
 
 V7only [
 Syntactic Definition allT := all.
+Syntactic Definition inst := Logic.inst.
+Syntactic Definition gen := Logic.gen.
 ].
 
+(*
 Section universal_quantification.
 
 Variable A : Type.
@@ -45,7 +48,9 @@ Red; Auto.
 Qed.
 
 End universal_quantification.
+*)
 
+(*
 (** * Existential Quantification *)
 
 (** [exT A P], or simply [(EXT x | P(x))], stands for the existential 
@@ -54,7 +59,6 @@ End universal_quantification.
 (** [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the
     existential quantification on both [P] and [Q] when [A] is of
     type [Type] *)
-(*
 Inductive  exT [A:Type;P:A->Prop] : Prop
     := exT_intro : (x:A)(P x)->(exT A P).
 *)
@@ -76,6 +80,7 @@ Syntactic Definition exT_intro2 := ex_intro2.
 Syntactic Definition exT2_ind  := ex2_ind.
 ].
 
+(*
 (** Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y)
 
    [eqT A x y], or simply [x==y], is Leibniz' equality when [A] is of 
@@ -83,7 +88,6 @@ Syntactic Definition exT2_ind  := ex2_ind.
    symmetry, transitivity and stability by congruence *)
 
 
-(*
 Inductive eqT [A:Type;x:A] : A -> Prop
                        := refl_eqT : (eqT A x x).
 
@@ -107,22 +111,22 @@ Section Equality_is_a_congruence.
  
  Lemma sym_eqT : (eqT ? x y) -> (eqT ? y x).
  Proof.
-  Induction 1; Trivial.
+  NewDestruct 1; Trivial.
  Qed.
 
  Lemma trans_eqT : (eqT ? x y) -> (eqT ? y z) -> (eqT ? x z).
  Proof.
-  Induction 2; Trivial.
+  NewDestruct 2; Trivial.
  Qed.
 
  Lemma congr_eqT : (eqT ? x y)->(eqT ? (f x) (f y)).
  Proof.
-  Induction 1; Trivial.
+  NewDestruct 1; Trivial.
  Qed.
 
  Lemma sym_not_eqT : ~(eqT ? x y) -> ~(eqT ? y x).
  Proof.
-  Red; Intros H H'; Apply H; Elim H'; Trivial.
+  Red; Intros H H'; Apply H; NewDestruct H'; Trivial.
  Qed.
 
 End Equality_is_a_congruence.
@@ -183,22 +187,22 @@ Section IdentityT_is_a_congruence.
  
  Lemma sym_idT : (identityT ? x y) -> (identityT ? y x).
  Proof.
-  Induction 1; Trivial.
+  NewDestruct 1; Trivial.
  Qed.
 
  Lemma trans_idT : (identityT ? x y) -> (identityT ? y z) -> (identityT ? x z).
  Proof.
-  Induction 2; Trivial.
+  NewDestruct 2; Trivial.
  Qed.
 
  Lemma congr_idT : (identityT ? x y)->(identityT ? (f x) (f y)).
  Proof.
-  Induction 1; Trivial.
+  NewDestruct 1; Trivial.
  Qed.
 
  Lemma sym_not_idT : (notT (identityT ? x y)) -> (notT (identityT ? y x)).
  Proof.
-  Red; Intros H H'; Apply H; Elim H'; Trivial.
+  Red; Intros H H'; Apply H; NewDestruct H'; Trivial.
  Qed.
 
 End IdentityT_is_a_congruence.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
new file mode 100644
index 000000000..9fe617136
--- /dev/null
+++ b/theories/Init/Notations.v
@@ -0,0 +1,92 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** These are the notations whose level and associativity is imposed by Coq *)
+
+(** Notations for logical connectives *)
+
+Uninterpreted Notation "x /\ y" (at level 6, right associativity).
+Uninterpreted Notation "x \/ y" (at level 7, right associativity).
+
+Uninterpreted Notation "x <-> y" (at level 8, right associativity).
+
+Uninterpreted Notation "~ x" (at level 5, right associativity)
+  V8only (at level 55, right associativity).
+
+(** Notations for equality and inequalities *)
+
+Uninterpreted Notation "x = y  :> T" 
+  (at level 5, y at next level, no associativity).
+Uninterpreted Notation "x = y"
+  (at level 5, no associativity).
+
+Uninterpreted Notation "x <> y  :> T" 
+  (at level 5, y at next level, no associativity).
+Uninterpreted Notation "x <> y"
+  (at level 5, no associativity).
+
+Uninterpreted Notation "x <= y" (at level 5, no associativity).
+Uninterpreted Notation "x < y" (at level 5, no associativity).
+Uninterpreted Notation "x >= y" (at level 5, no associativity).
+Uninterpreted Notation "x > y" (at level 5, no associativity).
+
+(** Arithmetical notations (also used for type constructors) *)
+
+Uninterpreted Notation "x * y" (at level 3, right associativity)
+  V8only (at level 30, left associativity).
+Uninterpreted Notation "x / y" (at level 3, left associativity).
+Uninterpreted Notation "x + y" (at level 4, left associativity).
+Uninterpreted Notation "x - y" (at level 4, left associativity).
+Uninterpreted Notation "- x" (at level 0) V8only (at level 40).
+
+(** Notations for pairs *)
+
+Uninterpreted Notation "( x , y )" (at level 0)
+  V8only "x , y" (at level 150, left associativity).
+
+(** Notations for sum-types *)
+
+(* Home-made factorization at level 4 to parse B+{x:A|P} without parentheses *)
+
+Uninterpreted Notation "B + { x : A | P }"
+  (at level 4, left associativity, only parsing)
+  V8only (at level 40, x at level 80, left associativity, only parsing).
+
+Uninterpreted Notation "B + { x : A | P & Q }"
+  (at level 4, left associativity, only parsing)
+  V8only (at level 40, x at level 80, left associativity, only parsing).
+
+Uninterpreted Notation "B + { x : A & P }"
+  (at level 4, left associativity, only parsing)
+  V8only (at level 40, x at level 80, left associativity, only parsing).
+
+Uninterpreted Notation "B + { x : A & P & Q }"
+  (at level 4, left associativity, only parsing)
+  V8only (at level 40, x at level 80, left associativity, only parsing).
+
+(* At level 1 to factor with {x:A|P} etc *)
+
+Uninterpreted Notation "{ A } + { B }" (at level 1)
+  V8only (at level 10, A at level 80).
+
+Uninterpreted Notation "A + { B }" (at level 4, left associativity)
+  V8only (at level 40, B at level 80, left associativity).
+
+(** Notations for sigma-types or subsets *)
+
+Uninterpreted Notation "{ x : A  |  P }" (at level 1)
+  V8only (at level 10, x at level 80).
+Uninterpreted Notation "{ x : A  |  P  &  Q }" (at level 1)
+  V8only (at level 10, x at level 80).
+
+Uninterpreted Notation "{ x : A  &  P }" (at level 1)
+  V8only (at level 10, x at level 80).
+Uninterpreted Notation "{ x : A  &  P  &  Q }" (at level 1)
+  V8only (at level 10, x at level 80).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 5f6d2d8a8..55e44d28d 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -23,6 +23,7 @@
    including Peano's axioms of arithmetic (in Coq, these are in fact provable)
    Case analysis on [nat] and induction on [nat * nat] are provided too *)
 
+Require Notations.
 Require Logic.
 Require LogicSyntax.
 Require Datatypes.
@@ -65,13 +66,13 @@ Theorem O_S : (n:nat)~(O=(S n)).
 Proof.
   Red;Intros n H.
   Change (IsSucc O).
-  Elim (sym_eq nat O (S n));[Exact I | Assumption].
+  Rewrite <- (sym_eq nat O (S n));[Exact I | Assumption].
 Qed.
 Hints Resolve O_S : core v62.
 
 Theorem n_Sn : (n:nat) ~(n=(S n)).
 Proof.
-  Induction n ; Auto.
+  NewInduction n ; Auto.
 Qed.
 Hints Resolve n_Sn : core v62.
 
@@ -86,7 +87,7 @@ Hint eq_nat_binary : core := Resolve (f_equal2 nat nat).
 
 Lemma plus_n_O : (n:nat) n=(plus n O).
 Proof.
-  Induction n ; Simpl ; Auto.
+  NewInduction n ; Simpl ; Auto.
 Qed.
 Hints Resolve plus_n_O : core v62.
 
@@ -97,7 +98,7 @@ Qed.
 
 Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)).
 Proof.
-  Intros m n; Elim m; Simpl; Auto.
+  Intros n m; NewInduction n; Simpl; Auto.
 Qed.
 Hints Resolve plus_n_Sm : core v62.
 
@@ -115,14 +116,14 @@ Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult).
 
 Lemma mult_n_O : (n:nat) O=(mult n O).
 Proof.
-  Induction n; Simpl; Auto.
+  NewInduction n; Simpl; Auto.
 Qed.
 Hints Resolve mult_n_O : core v62.
 
 Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
 Proof.
-  Intros; Elim n; Simpl; Auto.
-  Intros p H; Case H; Elim plus_n_Sm; Apply (f_equal nat nat S).
+  Intros; NewInduction n as [|p H]; Simpl; Auto.
+  NewDestruct H; Rewrite <- plus_n_Sm; Apply (f_equal nat nat S).
   Pattern 1 3 m; Elim m; Simpl; Auto.
 Qed.
 Hints Resolve mult_n_Sm : core v62.
@@ -161,7 +162,7 @@ Hints Unfold gt : core v62.
 
 Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n).
 Proof.
-  Induction n ; Auto.
+  NewInduction n ; Auto.
 Qed.
 
 (** Principle of double induction *)
@@ -171,8 +172,8 @@ Theorem nat_double_ind : (R:nat->nat->Prop)
      -> ((n,m:nat)(R n m)->(R (S n) (S m)))
      -> (n,m:nat)(R n m).
 Proof.
-  Induction n; Auto.
-  Induction m; Auto.
+  NewInduction n; Auto.
+  NewDestruct m; Auto.
 Qed.
 
 (** Notations *)
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 030ab339e..7577fe486 100755
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -8,6 +8,7 @@
 
 (*i $Id$ i*)
 
+Require Export Notations.
 Require Export Datatypes.
 Require Export DatatypesSyntax.
 Require Export Logic.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 77b9980f9..c9617362d 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -17,30 +17,38 @@ Require Datatypes.
 Require Logic.
 Require LogicSyntax.
 
-Section Subsets.
+(** Subsets *)
 
- (** [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset 
-     of elements of the Set [A] which satisfy the predicate [P].
-     Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset 
-     of elements of the Set [A] which satisfy both [P] and [Q]. *)
+(** [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset 
+    of elements of the Set [A] which satisfy the predicate [P].
+    Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset 
+    of elements of the Set [A] which satisfy both [P] and [Q]. *)
 
-  Inductive sig [A:Set;P:A->Prop] : Set
-      := exist : (x:A)(P x) -> (sig A P).
+Inductive sig [A:Set;P:A->Prop] : Set
+    := exist : (x:A)(P x) -> (sig A P).
 
-  Inductive sig2 [A:Set;P,Q:A->Prop] : Set
-      := exist2 : (x:A)(P x) -> (Q x) -> (sig2 A P Q).
+Inductive sig2 [A:Set;P,Q:A->Prop] : Set
+    := exist2 : (x:A)(P x) -> (Q x) -> (sig2 A P Q).
 
- (** [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant
-     of subset where [P] is now of type [Set].
-     Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
+(** [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant
+    of subset where [P] is now of type [Set].
+    Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
      
-  Inductive sigS [A:Set;P:A->Set] : Set
-      := existS : (x:A)(P x) -> (sigS A P).
+Inductive sigS [A:Set;P:A->Set] : Set
+    := existS : (x:A)(P x) -> (sigS A P).
 
-  Inductive sigS2 [A:Set;P,Q:A->Set] : Set
-      := existS2 : (x:A)(P x) -> (Q x) -> (sigS2 A P Q).
+Inductive sigS2 [A:Set;P,Q:A->Set] : Set
+    := existS2 : (x:A)(P x) -> (Q x) -> (sigS2 A P Q).
 
-End Subsets.
+Arguments Scope sig [type_scope type_scope].
+Arguments Scope sig2 [type_scope type_scope type_scope].
+Arguments Scope sigS [type_scope type_scope].
+Arguments Scope sigS2 [type_scope type_scope type_scope].
+
+Notation "{ x : A  |  P }" := (sig A [x:A]P).
+Notation "{ x : A  |  P  &  Q }" := (sig2 A [x:A]P [x:A]Q).
+Notation "{ x : A  &  P }" := (sigS A [x:A]P).
+Notation "{ x : A  &  P  &  Q }" := (sigS2 A [x:A]P [x:A]Q).
 
 Add Printing Let sig.
 Add Printing Let sig2.
@@ -86,20 +94,21 @@ Section Projections.
 End Projections.
 
 
-Section Extended_booleans.
+(** Extended_booleans *)
 
-  (** Syntax sumbool ["{_}+{_}"]. *)
-  Inductive sumbool [A,B:Prop] : Set
-      := left  : A -> (sumbool A B) 
-       | right : B -> (sumbool A B).
+Inductive sumbool [A,B:Prop] : Set as "{ A } + { B }"
+    := left  : A -> {A}+{B}
+     | right : B -> {A}+{B}.
 
+(*
   (** Syntax sumor ["_+{_}"]. *)
   Inductive sumor [A:Set;B:Prop] : Set
       := inleft  : A -> (sumor A B) 
        | inright : B -> (sumor A B).
-
-
-End Extended_booleans.
+*)
+Inductive sumor [A:Set;B:Prop] : Set as "A + { B }"
+    := inleft  : A -> A+{B}
+     | inright : B -> A+{B}.
 
 
 (** Choice *)
@@ -118,7 +127,7 @@ Section Choice_lemmas.
   Proof.
    Intro H.
    Exists [z:S]Cases (H z) of (exist y _) => y end.
-   Intro z; Elim (H z); Trivial.
+   Intro z; NewDestruct (H z); Trivial.
   Qed.
 
   Lemma Choice2 : ((x:S)(sigS ? [y:S'](R' x y))) ->
@@ -126,7 +135,7 @@ Section Choice_lemmas.
   Proof.
     Intro H.
     Exists [z:S]Cases (H z) of (existS y _) => y end.
-    Intro z; Elim (H z); Trivial.
+    Intro z; NewDestruct (H z); Trivial.
   Qed.
 
   Lemma bool_choice : 
@@ -136,7 +145,7 @@ Section Choice_lemmas.
   Proof.
     Intro H.
     Exists [z:S]Cases (H z) of (left _) => true | (right _) => false end.
-    Intro z; Elim (H z); Auto.
+    Intro z; NewDestruct (H z); Auto.
   Qed.
 
 End Choice_lemmas.
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 0591f081b..627771fc4 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -8,6 +8,7 @@
 
 (*i $Id$ i*)
 
+Require Notations.
 Require Datatypes.
 Require Specif.
 
@@ -15,30 +16,17 @@ Require Specif.
 
 (* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
 
-Notation "B + { x : A | P }"     := B + (sig A [x:A]P)
-  (at level 4, left associativity, only parsing)
-  V8only (at level 40, x at level 80, left associativity, only parsing).
+Notation "B + { x : A | P }"     := B + (sig A [x:A]P) (only parsing).
+Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) (only parsing).
+Notation "B + { x : A & P }"     := B + (sigS A [x:A]P) (only parsing).
+Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) (only parsing).
 
-Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q)
-  (at level 4, left associativity, only parsing)
-  V8only (at level 40, x at level 80, left associativity, only parsing).
+(** Symbolic notations for definitions in [Specif.v] *)
 
-Notation "B + { x : A & P }"     := B + (sigS A [x:A]P)
-  (at level 4, left associativity, only parsing)
-  V8only (at level 40, x at level 80, left associativity, only parsing).
-
-Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q)
-  (at level 4, left associativity, only parsing)
-  V8only (at level 40, x at level 80, left associativity, only parsing).
-
-(** Symbolic notations for things in [Specif.v] *)
-
-(* At level 1 to factor with {x:A|P} etc *)
-Notation "{ A } + { B }" := (sumbool A B) (at level 1)
-  V8only (at level 10, A at level 80).
-
-Notation "A + { B }" := (sumor A B) (at level 4, left associativity)
-  V8only (at level 40, B at level 80, left associativity).
+(*
+Notation "{ A } + { B }" := (sumbool A B).
+Notation "A + { B }" := (sumor A B).
+*)
 
 Notation ProjS1 := (projS1 ? ?).
 Notation ProjS2 := (projS2 ? ?).
@@ -46,18 +34,3 @@ Notation Except := (except ?).
 Notation Error := (error ?).
 Notation Value := (value ?).
 
-Arguments Scope sig [type_scope type_scope].
-Arguments Scope sig2 [type_scope type_scope type_scope].
-
-Notation "{ x : A  |  P }"       := (sig A [x:A]P)          (at level 1)
-  V8only (at level 10, x at level 80).
-Notation "{ x : A  |  P  &  Q }" := (sig2 A [x:A]P [x:A]Q)  (at level 1)
-  V8only (at level 10, x at level 80).
-
-Arguments Scope sigS [type_scope type_scope].
-Arguments Scope sigS2 [type_scope type_scope type_scope].
-
-Notation "{ x : A  &  P }"       := (sigS A [x:A]P)         (at level 1)
-  V8only (at level 10, x at level 80).
-Notation "{ x : A  &  P  &  Q }" := (sigS2 A [x:A]P [x:A]Q) (at level 1)
-  V8only (at level 10, x at level 80).
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 11d213202..dff48c953 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -111,19 +111,19 @@ Scheme Acc_inv_dep := Induction for Acc Sort Prop.
 Lemma Fix_F_eq
   : (x:A)(r:(Acc x))
     (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p)))=(Fix_F x r).
-Intros x r; Elim r using  Acc_inv_dep; Auto.
+NewDestruct r using  Acc_inv_dep; Auto.
 Qed.
 
 Lemma Fix_F_inv : (x:A)(r,s:(Acc x))(Fix_F x r)=(Fix_F x s).
-Intro x; Elim (Rwf x); Intros.
-Case (Fix_F_eq x0 r); Case (Fix_F_eq x0 s); Intros.
+Intro x; NewInduction (Rwf x); Intros.
+Rewrite <- (Fix_F_eq x r); Rewrite <- (Fix_F_eq x s); Intros.
 Apply F_ext; Auto.
 Qed.
 
 
 Lemma Fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)).
-Intro; Unfold fix.
-Case (Fix_F_eq x).
+Intro x; Unfold fix.
+Rewrite <- (Fix_F_eq x).
 Apply F_ext; Intros.
 Apply Fix_F_inv.
 Qed.
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 8a7a1caa4..414a230f0 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -546,7 +546,7 @@ Qed.
 
   Lemma Zgt_is_le_bool : (x,y:Z) (Zgt x y) <-> (Zle_bool y `x-1`)=true.
   Proof.
-    Intros. Apply iff_trans with b:=`y < x`. Split. Exact (Zgt_lt x y).
+    Intros. Apply iff_trans with `y < x`. Split. Exact (Zgt_lt x y).
     Exact (Zlt_gt y x).
     Exact (Zlt_is_le_bool y x).
   Qed.