diff options
| author | sacerdot | 2004-10-14 11:36:16 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-14 11:36:16 +0000 |
| commit | 6565c4ad7d6ab70bbb866cd2c1435f767820725e (patch) | |
| tree | f5e46d1a3bd42884fc16a23d6a56a2f4bd0e51ec /test-suite | |
| parent | 528bc9aa2b4134122caf0387cdf89f5ce592a11b (diff) | |
reflexivity, symmetry, symmetry ... in e transitivity now fall-back
to their setoid_* counterparts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6213 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/setoid_test.v8 | 2 | ||||
| -rw-r--r-- | test-suite/success/setoid_test2.v8 | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/test-suite/success/setoid_test.v8 b/test-suite/success/setoid_test.v8 index 5c62d12a14..574cb525a5 100644 --- a/test-suite/success/setoid_test.v8 +++ b/test-suite/success/setoid_test.v8 @@ -54,7 +54,7 @@ split; apply add_aux. assumption. rewrite H. -setoid_reflexivity. +reflexivity. Qed. Fixpoint remove (a : A) (s : set) {struct s} : set := diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8 index 72b9d03ce0..a4156c6805 100644 --- a/test-suite/success/setoid_test2.v8 +++ b/test-suite/success/setoid_test2.v8 @@ -61,6 +61,8 @@ Require Export Setoid. ### non capisce piu' le riscritture con uguaglianze quantificate (almeno nell'esempio di Marco) +### Bas Spitters: poter dichiarare che ogni variabile nel contesto di tipo + un setoid_function e' un morfismo ### unificare le varie check_... ### sostituire a Use_* una sola eccezione Optimize @@ -136,13 +138,13 @@ Add Morphism f : f_compat2. Admitted. Theorem test1: forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)). intros. rewrite H. - setoid_reflexivity. + reflexivity. Qed. Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)). intros. setoid_replace x with y. - setoid_reflexivity. + reflexivity. assumption. Qed. |