diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 0000000000000000000000000000000000000000..0937c4a9e4c0aecde06bef0db5e13b6c4f8855f6
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,32 @@
+# run tests with main build
+real-all: test
+
+# the test suite
+TESTFILES=$(wildcard tests/*.v)
+
+test: $(TESTFILES:.v=.vo)
+.PHONY: test
+
+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+
+# Can't use pipes because that discards error codes and dash provides no way to control that.
+# Also egrep errors if it doesn't match anything, we have to ignore that.
+# Oh Unix...
+REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
+
+tests/.coqdeps.d: $(TESTFILES)
+	$(SHOW)'COQDEP TESTFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
+-include tests/.coqdeps.d
+
+$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
+	$(SHOW)$(if $(MAKE_REF),COQTEST [ref],COQTEST) $<
+	$(HIDE)TEST="$$(basename -s .v $<)" && \
+	  TMPFILE="$$(mktemp)" && \
+	  $(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+	  ($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
+	  $(if $(MAKE_REF), \
+	    mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
+	    diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered") && \
+	  rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
+	  touch $@
diff --git a/tests/solve_proper.ref b/tests/solve_proper.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/solve_proper.v b/tests/solve_proper.v
new file mode 100644
index 0000000000000000000000000000000000000000..1f44e13d742222f0d06cc8c5b441163592d5222e
--- /dev/null
+++ b/tests/solve_proper.v
@@ -0,0 +1,24 @@
+From stdpp Require Import prelude.
+
+(** Some tests for solve_proper. *)
+Section tests.
+  Context {A B : Type} `{!Equiv A, !Equiv B}.
+  Context (foo : A → A) (bar : A → B) (baz : B → A → A).
+  Context `{!Proper ((≡) ==> (≡)) foo,
+            !Proper ((≡) ==> (≡)) bar,
+            !Proper ((≡) ==> (≡) ==> (≡)) baz}.
+
+  Definition test1 (x : A) := baz (bar (foo x)) x.
+  Global Instance : Proper ((≡) ==> (≡)) test1.
+  Proof. solve_proper. Qed.
+
+  Definition test2 (b : bool) (x : A) :=
+    if b then bar (foo x) else bar x.
+  Global Instance : ∀ b, Proper ((≡) ==> (≡)) (test2 b).
+  Proof. solve_proper. Qed.
+
+  Definition test3 (f : nat → A) :=
+    baz (bar (f 0)) (f 2).
+  Global Instance : Proper (pointwise_relation nat (≡) ==> (≡)) test3.
+  Proof. solve_proper. Qed.
+End tests.
diff --git a/tests/typeclasses.ref b/tests/typeclasses.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/typeclasses.v b/tests/typeclasses.v
new file mode 100644
index 0000000000000000000000000000000000000000..6e31f52974a54dcbc9025cbc40b4e69ac3e25bf6
--- /dev/null
+++ b/tests/typeclasses.v
@@ -0,0 +1,17 @@
+From stdpp Require Import prelude.
+
+(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
+    Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
+    we cannot [1].  So at least we try to make sure the first solution found
+    is the right one, to not pay performance in the success case [2].
+
+    [1] https://github.com/coq/coq/issues/7916
+    [2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
+*)
+Lemma test_setoid_rewrite :
+  exists R, @Reflexive Prop R /\ R = iff.
+Proof.
+  eexists. split.
+  - apply _.
+  - reflexivity.
+Qed.