From 4fd77a7caa5fe6e88d04ad6bb9ce4e43f5f9bd89 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Thu, 30 Sep 2004 17:21:01 +0000
Subject: 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
---
 test-suite/success/setoid_test2.v8 | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8
index 86f54406e3..65b3973edd 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???
-- 
cgit v1.2.3