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 653b5bf9..be0d49e0 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -153,7 +153,7 @@ End mult.
does not fix the instance at the first unification, use [at], or simply rewrite for
this semantics. *)
-Require Import Arith.
+Parameter beq_nat : forall x y : nat, bool.
Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}.
Instance: Foo nat. admit. Defined.