Suppression des alias eqT/exT/exT2 en nouvelle syntaxe

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

2 files changed, 14 insertions, 0 deletions

diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index de4d2721f..b5a6e6038 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -22,7 +22,9 @@ Require LogicSyntax.
 Definition allT := [A:Type][P:A->Prop](x:A)(P x). 
 *)
 
+V7only [
 Syntactic Definition allT := all.
+].
 
 Section universal_quantification.
 
@@ -54,18 +56,22 @@ Inductive  exT [A:Type;P:A->Prop] : Prop
     := exT_intro : (x:A)(P x)->(exT A P).
 *)
 
+V7only [
 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).
 *)
 
+V7only [
 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)
 
@@ -80,11 +86,13 @@ Inductive eqT [A:Type;x:A] : A -> Prop
 
 Hints Resolve refl_eqT (* exT_intro2 exT_intro *) : core v62.
 *)
+V7only [
 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.
@@ -116,10 +124,12 @@ Section Equality_is_a_congruence.
 
 End Equality_is_a_congruence.
 *)
+V7only [
 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.
@@ -141,9 +151,11 @@ Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
 *)
 
+V7only [
 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 fa5ab26f8..6eb768ef0 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -12,6 +12,7 @@ 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).
 
@@ -36,6 +37,7 @@ Notation "'EXT' x | p & q"     := (ex2 ? [x]p [x]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] *)