diff options
| -rw-r--r-- | test-suite/success/setoid_test.v | 2 | ||||
| -rw-r--r-- | test-suite/success/setoid_test_function_space.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index a7818f6f6..f49f58e5a 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -18,7 +18,7 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t. Lemma setoid_set : Setoid_Theory set same. -unfold same in |- *; split. +unfold same in |- *; split ; red. red in |- *; auto. red in |- *. diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v index 2e9bd60ea..ead93d913 100644 --- a/test-suite/success/setoid_test_function_space.v +++ b/test-suite/success/setoid_test_function_space.v @@ -26,7 +26,7 @@ Hint Unfold feq. Hint Resolve feq_refl feq_sym feq_trans. Variable K:(nat -> nat)->Prop. Variable K_ext:forall a b, (K a)->(a =f b)->(K b). -Add Relation (A -> B) (@feq A B) +Add Parametric Relation (A B : Type) : (A -> B) (@feq A B) reflexivity proved by (@feq_refl A B) symmetry proved by (@feq_sym A B) transitivity proved by (@feq_trans A B) as funsetoid. |