summaryrefslogtreecommitdiff
path: root/test-suite/success/setoid_test.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/setoid_test.v')
-rw-r--r--test-suite/success/setoid_test.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index be5999df..033b3f48 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -124,7 +124,7 @@ Goal forall
(f : Prop -> Prop)
(Q : (nat -> Prop) -> Prop)
(H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True)
- (h:nat -> Prop),
+ (h:nat -> Prop),
Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True.
intros f0 Q H.
setoid_rewrite H.