Fusion des fichiers de syntaxe de Init avec les fichiers de définition; TypeSyntax inutile

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

13 files changed, 101 insertions, 207 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 91ec84c424..c24b86426a 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -95,7 +95,7 @@ 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.
+(** First-order quantifiers *)
 
   (** [(ex A P)], or simply [(EX x | P(x))], expresses the existence of an 
       [x] of type [A] which satisfies the predicate [P] ([A] is of type 
@@ -110,15 +110,41 @@ Section First_order_quantifiers.
       construction [(all A P)], or simply [(All P)], is provided as an 
       abbreviation of [(x:A)(P x)] *) 
 
-  Inductive ex [A:Type;P:A->Prop] : Prop 
-      := ex_intro : (x:A)(P x)->(ex A P).
+Inductive ex [A:Type;P:A->Prop] : Prop 
+    := ex_intro : (x:A)(P x)->(ex A P).
 
-  Inductive ex2 [A:Type;P,Q:A->Prop] : Prop
-      := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q).
+Inductive ex2 [A:Type;P,Q:A->Prop] : Prop
+    := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q).
 
-  Definition all := [A:Type][P:A->Prop](x:A)(P x). 
+Definition all := [A:Type][P:A->Prop](x:A)(P x). 
 
-  Section universal_quantification.
+(*Rule order is important to give printing priority to fully typed ALL and EX*)
+
+V7only [ Notation Ex  := (ex ?). ].
+Notation "'EX' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
+  V8only (at level 200, x ident, p at level 80).
+Notation "'EX' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8)
+  V8only (at level 200, x ident, p at level 80).
+
+V7only [ Notation Ex2 := (ex2 ?). ].
+Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
+  (at level 10, p, q at level 8)
+  V8only "'EX2' x | p & q" (at level 200, x ident, p, q at level 80).
+Notation "'EX' x : t | p & q"   := (ex2 ? [x:t]p [x:t]q)
+  (at level 10, p, q at level 8)
+  V8only "'EX2' x : t | p & q"
+    (at level 200, x ident, t at level 200, p, q at level 80).
+
+V7only [Notation All := (all ?).].
+Notation "'ALL' x | p"     := (all ? [x]p)   (at level 10, p at level 8)
+  V8only (at level 200, x ident, p at level 200).
+Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8)
+  V8only (at level 200, x ident, t, p at level 200).
+
+
+(** Universal quantification *)
+
+Section universal_quantification.
 
   Variable A : Type.
   Variable P : A->Prop.
@@ -135,7 +161,7 @@ Section First_order_quantifiers.
 
   End universal_quantification.
 
-End First_order_quantifiers.
+(** Equality *)
 
 (** [(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].
@@ -249,3 +275,12 @@ Proof.
 Qed.
 
 Hints Immediate sym_eq sym_not_eq : core v62.
+
+V7only[
+(** Parsing only of things in [Logic.v] *)
+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/LogicSyntax.v b/theories/Init/LogicSyntax.v
deleted file mode 100644
index 53940f2371..0000000000
--- a/theories/Init/LogicSyntax.v
+++ /dev/null
@@ -1,66 +0,0 @@
-(***********************************************************************)
-(*  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*)
-
-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).
-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).
-
-Infix RIGHTA 6 "/\\" and.
-Infix RIGHTA 7 "\\/" or.
-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 *)
-
-V7only [ Notation All := (all ?). ].
-Notation "'ALL' x | p"     := (all ? [x]p)   (at level 10, p at level 8)
-  V8only (at level 200, p at level 200).
-Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8)
-  V8only (at level 200).
-
-V7only [ Notation Ex  := (ex ?). ].
-Notation "'EX' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
-  V8only (at level 200, x at level 80).
-Notation "'EX' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8)
-  V8only (at level 200, x at level 80).
-
-V7only [ Notation Ex2 := (ex2 ?). ].
-Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
-  (at level 10, p, q at level 8)
-  V8only "'EX2' x | p & q" (at level 200, x at level 80).
-Notation "'EX' x : t | p & q"   := (ex2 ? [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] *)
-
-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 e5416276b4..2064d585b7 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -14,10 +14,10 @@ V7only [Unset Implicit Arguments.].
 (** This module defines quantification on the world [Type]
     ([Logic.v] was defining it on the world [Set]) *)
 
+Require Notations.
 Require Export Logic.
-Require LogicSyntax.
-
 
+V7only [
 (*
 (** [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)]
    when [A] is of type [Type] *)
@@ -25,11 +25,15 @@ Require LogicSyntax.
 Definition allT := [A:Type][P:A->Prop](x:A)(P x). 
 *)
 
-V7only [
 Notation allT := all (only parsing).
 Notation inst := Logic.inst (only parsing).
 Notation gen := Logic.gen (only parsing).
-].
+
+(* Order is important to give printing priority to fully typed ALL and EX *)
+
+Notation AllT := (all ?).
+Notation "'ALLT' x | p"     := (all ? [x]p)   (at level 10, p at level 8).
+Notation "'ALLT' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8).
 
 (*
 Section universal_quantification.
@@ -63,22 +67,28 @@ Inductive  exT [A:Type;P:A->Prop] : Prop
     := exT_intro : (x:A)(P x)->(exT A P).
 *)
 
-V7only [
 Notation exT := ex (only parsing).
 Notation exT_intro := ex_intro (only parsing).
 Notation exT_ind  := ex_ind (only parsing).
-].
+
+Notation ExT  := (ex ?).
+Notation "'EXT' x | p"      := (ex ? [x]p)    (at level 10, p at level 8).
+Notation "'EXT' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8).
 
 (*
 Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
     := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q).
 *)
 
-V7only [
 Notation exT2 := ex2 (only parsing).
 Notation exT_intro2 := ex_intro2 (only parsing).
 Notation exT2_ind  := ex2_ind (only parsing).
-].
+
+Notation ExT2 := (ex2 ?).
+Notation "'EXT' x | p & q"     := (ex2 ? [x]p [x]q)
+  (at level 10, p, q at level 8).
+Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q)
+  (at level 10, p, q at level 8).
 
 (*
 (** Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y)
@@ -93,13 +103,19 @@ Inductive eqT [A:Type;x:A] : A -> Prop
 
 Hints Resolve refl_eqT (* exT_intro2 exT_intro *) : core v62.
 *)
-V7only [
+
 Notation eqT      := eq (only parsing).
 Notation refl_eqT := refl_equal (only parsing).
 Notation eqT_ind  := eq_ind (only parsing).
 Notation eqT_rect := eq_rect (only parsing).
 Notation eqT_rec  := eq_rec (only parsing).
-].
+
+Notation "x == y"  := (eq ? x y) (at level 5, no associativity, only parsing).
+
+(** Parsing only of things in [Logic_type.v] *)
+
+Notation "< A > x == y"  := (eq A x y)
+   (A annot, at level 1, x at level 0, only parsing).
 
 (*
 Section Equality_is_a_congruence.
@@ -131,12 +147,11 @@ Section Equality_is_a_congruence.
 
 End Equality_is_a_congruence.
 *)
-V7only [
+
 Notation sym_eqT  := sym_eq (only parsing).
 Notation trans_eqT  := trans_eq (only parsing).
 Notation congr_eqT  := f_equal (only parsing).
 Notation sym_not_eqT  := sym_not_eq (only parsing).
-].
 
 (*
 Hints Immediate sym_eqT sym_not_eqT : core v62.
@@ -158,7 +173,6 @@ Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
 *)
 
-V7only [
 Notation eqT_ind_r  := eq_ind_r (only parsing).
 Notation eqT_rec_r  := eq_rec_r (only parsing).
 Notation eqT_rect_r  := eq_rect_r (only parsing).
@@ -173,9 +187,18 @@ Definition notT := [A:Type] A->EmptyT.
 
 (** Have you an idea of what means [identityT A a b]? No matter! *)
 
-Inductive identityT [A:Type; a:A] : A->Type :=
+Uninterpreted Notation "x === y :> A"
+  (at level 5, y at next level, no associativity).
+
+Inductive identityT [A:Type; a:A] : (b:A)Type as "a === b :> A" :=
      refl_identityT : (identityT A a a).
 
+V7only [
+Notation "< A > x === y" := (!identityT A x y)
+   (A annot, at level 1, x at level 0, only parsing).
+].
+Notation "x === y" := (identityT ? x y) (at level 5, no associativity).
+
 Hints Resolve refl_identityT : core v62.
 
 Section IdentityT_is_a_congruence.
@@ -254,6 +277,8 @@ Definition prodT_curry : (A,B,C:Type)(A->B->C)->(prodT A B)->C :=
 
 Hints Immediate sym_idT sym_not_idT : core v62.
 
+V7only [
 Implicits fstT [1 2].
 Implicits sndT [1 2].
 Implicits pairT [1 2].
+].
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
deleted file mode 100644
index e48b150622..0000000000
--- a/theories/Init/Logic_TypeSyntax.v
+++ /dev/null
@@ -1,51 +0,0 @@
-(***********************************************************************)
-(*  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*)
-
-Require Notations.
-Require Logic_Type.
-
-(** Symbolic notations for things in [Logic_type.v] *)
-
-V7only [
-Notation "x == y"  := (eq ? x y) (at level 5, no associativity, only parsing).
-Notation "x === y" := (identityT ? x y) (at level 5, no associativity).
-
-(* Order is important to give printing priority to fully typed ALL and EX *)
-
-Notation AllT := (all ?).
-Notation "'ALLT' x | p"     := (all ? [x]p)   (at level 10, p at level 8)
-  V8only (at level 200, x at level 80).
-Notation "'ALLT' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8)
-  V8only (at level 200, x at level 80).
-
-Notation ExT  := (ex ?).
-Notation "'EXT' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
-  V8only (at level 200, x at level 80).
-Notation "'EXT' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8)
-  V8only (at level 200, x at level 80).
-
-Notation ExT2 := (ex2 ?).
-Notation "'EXT' x | p & q"     := (ex2 ? [x]p [x]q)
-  (at level 10, p, q at level 8)
-  V8only "'EXT2' x | p & q" (at level 200, x at level 80).
-Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q)
-  (at level 10, p, q at level 8)
-  V8only "'EXT2' x : t | p & q" (at level 200, x at level 80).
-].
-
-
-V7only[
-(** Parsing only of things in [Logic_type.v] *)
-Notation "< A > x == y"  := (eq A x y)
-   (A annot, at level 1, x at level 0, only parsing).
-
-Notation "< A > x === y" := (identityT A x y)
-   (A annot, at level 1, x at level 0, only parsing).
-].
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 41f26ffda9..0772260358 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -24,9 +24,8 @@
    Case analysis on [nat] and induction on [nat * nat] are provided too *)
 
 Require Notations.
-Require Logic.
-Require LogicSyntax.
 Require Datatypes.
+Require Logic.
 
 Open Local Scope nat_scope.
 
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 972a809866..e7ad28e3fe 100755
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -11,8 +11,6 @@
 Require Export Notations.
 Require Export Datatypes.
 Require Export Logic.
-Require Export LogicSyntax.
 Require Export Specif.
-Require Export SpecifSyntax.
 Require Export Peano.
 Require Export Wf.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index c9617362d8..7a05a89f75 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -13,9 +13,9 @@ V7only [Unset Implicit Arguments.].
 
 (** Basic specifications : Sets containing logical information *)
 
+Require Notations.
 Require Datatypes.
 Require Logic.
-Require LogicSyntax.
 
 (** Subsets *)
 
@@ -100,16 +100,16 @@ 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).
-*)
 Inductive sumor [A:Set;B:Prop] : Set as "A + { B }"
     := inleft  : A -> A+{B}
      | inright : B -> A+{B}.
 
+(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
+
+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).
 
 (** Choice *)
 
@@ -161,6 +161,9 @@ Definition error := None.
 
 Definition except := False_rec. (* for compatibility with previous versions *)
 
+Notation Except := (except ?).
+Notation Error := (error ?).
+
 Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C.
 Proof.
   Intros A C h1 h2.
@@ -188,3 +191,10 @@ Section projections_sigT.
                      Cases H of (existT x h) => h end.
 
 End projections_sigT.
+
+V7only [
+Notation ProjS1 := (projS1 ? ?).
+Notation ProjS2 := (projS2 ? ?).
+Notation Value := (value ?).
+].
+
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
deleted file mode 100644
index eb9c7cc495..0000000000
--- a/theories/Init/SpecifSyntax.v
+++ /dev/null
@@ -1,38 +0,0 @@
-(***********************************************************************)
-(*  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*)
-
-Require Notations.
-Require Datatypes.
-Require Specif.
-
-(** Extra factorization of parsing rules *)
-
-(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
-
-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).
-
-(** Symbolic notations for definitions in [Specif.v] *)
-
-(*
-Notation "{ A } + { B }" := (sumbool A B).
-Notation "A + { B }" := (sumor A B).
-*)
-
-V7only [
-Notation ProjS1 := (projS1 ? ?).
-Notation ProjS2 := (projS2 ? ?).
-Notation Value := (value ?).
-].
-
-Notation Except := (except ?).
-Notation Error := (error ?).
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 93111571f7..fbc71a3eaa 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -17,8 +17,8 @@ V7only [Unset Implicit Arguments.].
 
    from a well-founded ordering on a given set *)
 
+Require Notations.
 Require Logic.
-Require LogicSyntax.
 Require Datatypes.
 
 (** Well-founded induction principle on Prop *)
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index e90fa21480..4516a206f8 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -14,7 +14,6 @@
 
 Require Export ZArith_base.
 Require Export Rsyntax.
-Require Export TypeSyntax.
 V7only [Import R_scope.]. Open Local Scope R_scope.
 
 V7only [
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index d0c8e1f308..1df44bbf59 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -9,7 +9,6 @@
 (*i $Id$ i*)
 
 Require Export Rdefinitions.
-Require Export TypeSyntax.
 Require Export Raxioms.
 Require Export RIneq.
 Require Export DiscrR.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 96b682e048..c3f3ba5c92 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -14,7 +14,6 @@
 (*********************************************************)
 
 Require Export ZArith_base.
-Require Export TypeSyntax.
 
 Parameter R:Type.
 
diff --git a/theories/Reals/TypeSyntax.v b/theories/Reals/TypeSyntax.v
deleted file mode 100644
index 4653e6bb83..0000000000
--- a/theories/Reals/TypeSyntax.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(***********************************************************************)
-(*  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*)
-
-(*********************************************************)
-(*        Or and Exist in Type                           *)
-(*                                                       *)
-(*********************************************************)
-