eq fusionne avec eqT et devient par défaut sur Type,

idem pour ex et exT, ex2 et exT2, all et allT


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

3 files changed, 69 insertions, 30 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 7636204ab..ab78af469 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -99,13 +99,13 @@ 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:Set;P:A->Prop] : Prop 
+  Inductive ex [A:Type;P:A->Prop] : Prop 
       := ex_intro : (x:A)(P x)->(ex A P).
 
-  Inductive ex2 [A:Set;P,Q:A->Prop] : Prop
+  Inductive ex2 [A:Type;P,Q:A->Prop] : Prop
       := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q).
 
-  Definition all := [A:Set][P:A->Prop](x:A)(P x). 
+  Definition all := [A:Type][P:A->Prop](x:A)(P x). 
 
 End First_order_quantifiers.
 
@@ -117,7 +117,7 @@ Section Equality.
       The others properties (symmetry, transitivity, replacement of 
       equals) are proved below *)
 
-  Inductive eq [A:Set;x:A] : A->Prop
+  Inductive eq [A:Type;x:A] : A->Prop
          := refl_equal : (eq A x x).
 
 End Equality.
@@ -134,7 +134,7 @@ Section Logic_lemmas.
   Qed.
 
   Section equality.
-    Variable A,B : Set.
+    Variable A,B : Type.
     Variable f   : A->B.
     Variable x,y,z : A.
 
@@ -158,7 +158,7 @@ Section Logic_lemmas.
 
     Theorem sym_not_eq : (not (eq ? x y)) -> (not (eq ? y x)).
     Proof.
-     Red; Intros h1 h2; Apply h1; Elim h2; Trivial.
+     Red; Intros h1 h2; Apply h1; Case h2; Trivial.
     Qed.
 
     Definition sym_equal     := sym_eq.
@@ -168,7 +168,7 @@ Section Logic_lemmas.
   End equality.
 
 (* Is now a primitive principle 
-  Theorem eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
+  Theorem eq_rect: (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
   Proof.
    Intros.
    Cut (identity A x y).
@@ -177,33 +177,33 @@ Section Logic_lemmas.
   Qed.
 *)
 
-  Definition eq_ind_r : (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)(eq ? y x)->(P y).
-   Intros A x P H y H0; Case sym_eq with 1:= H0; Trivial.
+  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.
   Defined.
 
-  Definition eq_rec_r : (A:Set)(x:A)(P:A->Set)(P x)->(y:A)(eq ? y x)->(P y).
-    Intros A x P H y H0; Case sym_eq with 1:= H0; Trivial.
+  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.
   Defined.
 
-  Definition eq_rect_r : (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(eq ? y x)->(P y).
+  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.
   Defined.
 End Logic_lemmas.
 
-Theorem f_equal2 : (A1,A2,B:Set)(f:A1->A2->B)(x1,y1:A1)(x2,y2:A2)
+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.
 Qed.
 
-Theorem f_equal3 : (A1,A2,A3,B:Set)(f:A1->A2->A3->B)(x1,y1:A1)(x2,y2:A2)
+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.
 Qed.
 
-Theorem f_equal4 : (A1,A2,A3,A4,B:Set)(f:A1->A2->A3->A4->B)
+Theorem f_equal4 : (A1,A2,A3,A4,B:Type)(f:A1->A2->A3->A4->B)
   (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)(x4,y4:A4)
   (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4)
    -> (eq ? (f x1 x2 x3 x4) (f y1 y2 y3 y4)).
@@ -211,7 +211,7 @@ Proof.
   Induction 1; Induction 1; Induction 1; Induction 1; Trivial.
 Qed.
 
-Theorem f_equal5 : (A1,A2,A3,A4,A5,B:Set)(f:A1->A2->A3->A4->A5->B)
+Theorem f_equal5 : (A1,A2,A3,A4,A5,B:Type)(f:A1->A2->A3->A4->A5->B)
   (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)(x4,y4:A4)(x5,y5:A5)
   (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)).
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index e4982c1f6..de4d2721f 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -18,7 +18,11 @@ 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). 
+*)
+
+Syntactic Definition allT := all.
 
 Section universal_quantification.
 
@@ -27,7 +31,7 @@ Variable P : A->Prop.
 
 Theorem inst :  (x:A)(allT ? [x](P x))->(P x).
 Proof.
-Unfold allT; Auto.
+Unfold all; Auto.
 Qed.
 
 Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(allT A P).
@@ -45,12 +49,23 @@ 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).
+*)
+
+Syntactic Definition exT := ex.
+Syntactic Definition exT_intro := ex_intro.
+Syntactic Definition exT_ind  := ex_ind.
 
+(*
 Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
     := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q).
+*)
+
+Syntactic Definition exT2 := ex2.
+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)
 
@@ -58,11 +73,20 @@ Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
    type [Type]. This equality satisfies reflexivity (by definition), 
    symmetry, transitivity and stability by congruence *)
 
+
+(*
 Inductive eqT [A:Type;x:A] : A -> Prop
                        := refl_eqT : (eqT A x x).
 
-Hints Resolve refl_eqT exT_intro2 exT_intro : core v62.
+Hints Resolve refl_eqT (* exT_intro2 exT_intro *) : core v62.
+*)
+Syntactic Definition eqT      := eq.
+Syntactic Definition refl_eqT := refl_equal.
+Syntactic Definition eqT_ind  := eq_ind.
+Syntactic Definition eqT_rect := eq_rect.
+Syntactic Definition eqT_rec  := eq_rec.
 
+(*
 Section Equality_is_a_congruence.
 
  Variables A,B : Type.
@@ -91,11 +115,19 @@ Section Equality_is_a_congruence.
  Qed.
 
 End Equality_is_a_congruence.
+*)
+Syntactic Definition sym_eqT  := sym_eq.
+Syntactic Definition trans_eqT  := trans_eq.
+Syntactic Definition congr_eqT  := f_equal.
+Syntactic Definition sym_not_eqT  := sym_not_eq.
 
+(*
 Hints Immediate sym_eqT sym_not_eqT : core v62.
+*)
 
 (** This states the replacement of equals by equals *)
 
+(*
 Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
@@ -107,6 +139,11 @@ Defined.
 Definition eqT_rect_r : (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eqT ? y x)->(P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
+*)
+
+Syntactic Definition eqT_ind_r  := eq_ind_r.
+Syntactic Definition eqT_rec_r  := eq_rec_r.
+Syntactic Definition eqT_rect_r  := eq_rect_r.
 
 (** Some datatypes at the [Type] level *)
 
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 1de550267..9cebfb7df 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -12,35 +12,37 @@ Require Logic_Type.
 
 (** Symbolic notations for things in [Logic_type.v] *)
 
-Notation "x == y"  := (eqT ? x y)       (at level 5, no associativity).
+Notation "x == y"  := (eq ? x y) (at level 5, no associativity, only parsing).
 Notation "x === y" := (identityT ? x y) (at level 5, no associativity).
 
+Notation "'eqT'" := eq (at level 0).
+
 (* Order is important to give printing priority to fully typed ALL and EX *)
 
-Notation AllT := (allT ?).
-Notation "'ALLT' x | p"     := (allT ? [x]p)   (at level 10, p at level 8)
+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" := (allT t [x:t]p) (at level 10, p at level 8)
+Notation "'ALLT' x : t | p" := (all t [x:t]p) (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
 
-Notation ExT  := (exT ?).
-Notation "'EXT' x | p"      := (exT ? [x]p)    (at level 10, p at level 8)
+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"  := (exT t [x:t]p)  (at level 10, p at level 8)
+Notation "'EXT' x : t | p"  := (ex t [x:t]p)  (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
 
-Notation ExT2 := (exT2 ?).
-Notation "'EXT' x | p & q"     := (exT2 ? [x]p [x]q)
+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" := (exT2 t [x:t]p [x:t]q)
+Notation "'EXT' x : t | p & q" := (ex2 t [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).
 
 (** Parsing only of things in [Logic_type.v] *)
 
 V7only[
-Notation "< A > x == y"  := (eqT A x y)
+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)