diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-14 11:36:16 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-14 11:36:16 +0000 |
| commit | 6565c4ad7d6ab70bbb866cd2c1435f767820725e (patch) | |
| tree | f5e46d1a3bd42884fc16a23d6a56a2f4bd0e51ec /test-suite/success/setoid_test.v8 | |
| 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/success/setoid_test.v8')
| -rw-r--r-- | test-suite/success/setoid_test.v8 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/setoid_test.v8 b/test-suite/success/setoid_test.v8 index 5c62d12a1..574cb525a 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 := |