diff options
Diffstat (limited to 'test-suite/success/setoid_test2.v8')
| -rw-r--r-- | test-suite/success/setoid_test2.v8 | 6 |
1 files changed, 4 insertions, 2 deletions
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. |