Add some tests for backwards compatibility.

tests/proper.v

@@ -85,38 +85,34 @@ Section map_tests.
   that also allow the function to differ. We test that we can derive simpler
   [Proper]s for a fixed function using both type class inference ([apply _])
   and std++'s [solve_proper] tactic. *)
-  Global Instance map_zip_proper_test1 `{Equiv B} :
+  Global Instance map_zip_proper_test `{Equiv B} :
     Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
-  Proof. apply _. Abort.
-  Global Instance map_zip_proper_test2 `{Equiv B} :
-    Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
-  Proof. solve_proper. Abort.
-  Global Instance map_zip_with_proper_test1 `{Equiv B, Equiv C} (f : A → B → C) :
-    Proper ((≡) ==> (≡) ==> (≡)) f →
-    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
-  Proof. apply _. Qed.
-  Global Instance map_zip_with_proper_test2 `{Equiv B, Equiv C} (f : A → B → C) :
+  Proof. apply _. Restart. solve_proper. Abort.
+  Global Instance map_zip_with_proper_test `{Equiv B, Equiv C} (f : A → B → C) :
     Proper ((≡) ==> (≡) ==> (≡)) f →
     Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
-  Proof. solve_proper. Abort.
-  Global Instance map_fmap_proper_test1 `{Equiv B} (f : A → B) :
-    Proper ((≡) ==> (≡)) f →
-    Proper ((≡) ==> (≡@{M _})) (fmap f).
-  Proof. apply _. Qed.
-  Global Instance map_fmap_proper_test2 `{Equiv B} (f : A → B) :
+  Proof. apply _. Restart. solve_proper. Abort.
+  Global Instance map_fmap_proper_test `{Equiv B} (f : A → B) :
     Proper ((≡) ==> (≡)) f →
     Proper ((≡) ==> (≡@{M _})) (fmap f).
-  Proof. solve_proper. Qed.
-  Global Instance map_omap_proper_test1 `{Equiv B} (f : A → option B) :
-    Proper ((≡) ==> (≡)) f →
-    Proper ((≡) ==> (≡@{M _})) (omap f).
-  Proof. apply _. Qed.
-  Global Instance map_omap_proper_test2 `{Equiv B} (f : A → option B) :
+  Proof. apply _. Restart. solve_proper. Abort.
+  Global Instance map_omap_proper_test `{Equiv B} (f : A → option B) :
     Proper ((≡) ==> (≡)) f →
     Proper ((≡) ==> (≡@{M _})) (omap f).
-  Proof. solve_proper. Qed.
+  Proof. apply _. Restart. solve_proper. Abort.
 End map_tests.
 
+(** And similarly for lists *)
+Global Instance list_fmap_proper_test `{!Equiv A, !Equiv B} (f : A → B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f).
+Proof. apply _. Restart. solve_proper. Abort.
+Global Instance list_bind_proper_test `{!Equiv A, !Equiv B} (f : A → list B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mbind f).
+Proof. apply _. Restart. solve_proper. Abort.
+Global Instance mapM_proper_test `{!Equiv A, !Equiv B} (f : A → option B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mapM f).
+Proof. apply _. Restart. solve_proper. Abort.
+
 Lemma test_prod_equivalence (X1 X2 X3 Y : propset nat * propset nat) :
   X3 ≡ X2 → X2 ≡ X1 → (X1,Y) ≡ (X3,Y).
 Proof. intros H1 H2. by rewrite H1, <-H2. Qed.