diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-30 17:21:01 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-30 17:21:01 +0000 |
| commit | 4fd77a7caa5fe6e88d04ad6bb9ce4e43f5f9bd89 (patch) | |
| tree | 6d0668b08cf0d747888eef528ad42a5772f983d2 /test-suite/success | |
| parent | 8a00bdd6d838f65601ed9006671a8afcb9a1890d (diff) | |
New tactic
setoid_replace ... with ... in ... [using relation ...]
[generate side conditions ...]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6166 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/setoid_test2.v8 | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8 index 86f54406e..65b3973ed 100644 --- a/test-suite/success/setoid_test2.v8 +++ b/test-suite/success/setoid_test2.v8 @@ -50,10 +50,9 @@ Require Export Setoid. nessuna marcatura viene trovata Implementare: - -1. user-defined subrelations && user-proved subrelations - 0. trucco di Bruno - 2. setoid_replace ... with ... in ... - 4. [setoid_]symmetry, [setoid_]reflexivity, [setoid_]transitivity (?!?) + -2. user-defined subrelations && user-proved subrelations + -1. trucco di Bruno + 0. [setoid_]symmetry, [setoid_]reflexivity, [setoid_]transitivity (?!?) Sorgenti di inefficacia: 1. scelta del setoide di default per un sostegno: per farlo velocemente @@ -88,7 +87,7 @@ Require Export Setoid. l'uguaglianza di Leibniz. (Se entrambi sono uguaglianze di Leibniz allora il setoide e' una semplice funzione). ?10. [setoid_]rewrite ... in ... - setoid_replace ... in + setoid_replace ... in ... [setoid_]reflexivity??? [setoid_]transitivity??? [setoid_]symmetry??? |