Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8

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

1 files changed, 0 insertions, 105 deletions

diff --git a/test-suite/success/setoid_test.v8 b/test-suite/success/setoid_test.v8
deleted file mode 100644
index 574cb525a..000000000
--- a/test-suite/success/setoid_test.v8
+++ /dev/null
@@ -1,105 +0,0 @@
-Require Import Setoid.
-
-Parameter A : Set.
-
-Axiom eq_dec : forall a b : A, {a = b} + {a <> b}.
-
-Inductive set : Set :=
-  | Empty : set
-  | Add : A -> set -> set.
-
-Fixpoint In (a : A) (s : set) {struct s} : Prop :=
-  match s with
-  | Empty => False
-  | Add b s' => a = b \/ In a s'
-  end.
-
-Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t.
-
-Lemma setoid_set : Setoid_Theory set same.
-
-unfold same in |- *; split.
-red in |- *; auto.
-
-red in |- *.
-intros.
-elim (H a); auto.
-
-intros.
-elim (H a); elim (H0 a).
-split; auto.
-Qed.
-
-Add Setoid set same setoid_set as setsetoid.
-
-Add Morphism In : In_ext.
-unfold same in |- *; intros a s t H; elim (H a); auto.
-Qed.
-
-Lemma add_aux :
- forall s t : set,
- same s t -> forall a b : A, In a (Add b s) -> In a (Add b t).
-unfold same in |- *; simple induction 2; intros.
-rewrite H1.
-simpl in |- *; left; reflexivity.
-
-elim (H a).
-intros.
-simpl in |- *; right.
-apply (H2 H1).
-Qed.
-
-Add Morphism Add : Add_ext.
-split; apply add_aux.
-assumption.
-
-rewrite H.
-reflexivity.
-Qed.
-
-Fixpoint remove (a : A) (s : set) {struct s} : set :=
-  match s with
-  | Empty => Empty
-  | Add b t =>
-      match eq_dec a b with
-      | left _ => remove a t
-      | right _ => Add b (remove a t)
-      end
-  end.
-
-Lemma in_rem_not : forall (a : A) (s : set), ~ In a (remove a (Add a Empty)).
-
-intros.
-setoid_replace (remove a (Add a Empty)) with Empty.
-
-auto.
-
-unfold same in |- *.
-split.
-simpl in |- *.
-case (eq_dec a a).
-intros e ff; elim ff.
-
-intros; absurd (a = a); trivial.
-
-simpl in |- *.
-intro H; elim H.
-Qed.
-
-Parameter P : set -> Prop.
-Parameter P_ext : forall s t : set, same s t -> P s -> P t.
-
-Add Morphism P : P_extt.
-intros; split; apply P_ext; (assumption || apply (Seq_sym _ _ setoid_set); assumption).
-Qed.
-
-Lemma test_rewrite :
- forall (a : A) (s t : set), same s t -> P (Add a s) -> P (Add a t).
-intros.
-rewrite <- H.
-rewrite H.
-setoid_rewrite <- H.
-setoid_rewrite H.
-setoid_rewrite <- H.
-trivial.
-Qed.