Merge pull request #20 from coq-community/deprecation-8.20

Fix deprecations of auto using in Coq 8.20

.github/workflows/docker-action.yml

@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.20'
           - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'

Cut.v

@@ -172,7 +172,7 @@ Proof.
   destruct (Q_dec q r) as [[E1 | E2] | E3].
   - assumption.
   - exfalso. apply (disjoint x r).
-    auto using (lower_lower x r q).
+    pose (lower_lower x r q); auto.
   - exfalso. apply (disjoint x r).
     split; [idtac | assumption].
     rewrite <- E3; assumption.

MinMax.v

@@ -26,9 +26,9 @@ Proof.
     split.
     + destruct (Q.min_spec q r) as [[G H]|[G H]].
       * setoid_rewrite H ; assumption.
-      * setoid_rewrite H. auto using (lower_le x r q).
+      * setoid_rewrite H. pose (lower_le x r q); auto.
     + destruct (Q.min_spec q r) as [[G H]|[G H]].
-      * setoid_rewrite H. auto using (lower_lower y q r).
+      * setoid_rewrite H. pose (lower_lower y q r); auto.
       * setoid_rewrite H ; assumption.
   - destruct (upper_bound y) as [r ?].
     exists r.
@@ -89,8 +89,8 @@ Proof.
     apply neg_false.
     split.
     + intros [[lx ly] [ux | uy]].
-      auto using (disjoint x q).
-      auto using (disjoint y q).
+      pose (disjoint x q); auto.
+      pose (disjoint y q); auto.
     + tauto.
   - intros q r T.
     assert (H:=(located x q r T)).
@@ -113,11 +113,11 @@ Proof.
     exists (Qmax q r).
     split.
     + destruct (Q.max_spec q r) as [[G H]|[G H]].
-      * setoid_rewrite H. auto using (upper_upper x q r).
+      * setoid_rewrite H. pose (upper_upper x q r); auto.
       * setoid_rewrite H ; assumption.
     + destruct (Q.max_spec q r) as [[G H]|[G H]].
       * setoid_rewrite H ; assumption.
-      * setoid_rewrite H. auto using (upper_le y r q).
+      * setoid_rewrite H. pose (upper_le y r q); auto.
   - intros q r H [A | B].
     + assert (C:=(lower_lower x q r H A)).
       left ; assumption.
@@ -153,17 +153,17 @@ Proof.
     + destruct (Q.max_spec s q) as [[G H]|[G H]].
       * setoid_rewrite H ; assumption.
       * setoid_rewrite H.
-        auto using (upper_le x q s U G).
+        pose (upper_le x q s U G); auto.
     + destruct (Q.max_spec s q) as [[G H]|[G H]].
       * setoid_rewrite H.
-        auto using (upper_upper y s q G P).
+        pose (upper_upper y s q G P); auto.
       * setoid_rewrite H ; assumption.
   - intro.
     apply neg_false.
     split.
     + intros [[lx | ly] [ux  uy]].
-      auto using (disjoint x q).
-      auto using (disjoint y q).
+      pose (disjoint x q); auto.
+      pose (disjoint y q); auto.
     + tauto.
   - intros q r T.
     assert (H:=(located x q r T)).

Order.v

@@ -18,7 +18,7 @@ Ltac todo := apply unfinished.
 Theorem Rlt_irrefl : forall (x : R), ~ (x < x).
 Proof.
   intros x [q [H1 H2]].
-  auto using (disjoint x q).
+  pose (disjoint x q); auto.
 Qed.
 
 Theorem Rlt_trans : forall (x y z : R), x < y -> y < z -> x < z.
@@ -60,7 +60,7 @@ Qed.
 
 Theorem Rneq_irrefl : forall x : R, x ## x -> False.
 Proof.
-  intros x [A1|A2]; auto using (Rlt_irrefl x).
+  intros x [A1|A2]; pose (Rlt_irrefl x); auto.
 Qed.
 
 Theorem Rnew_contrans : forall x y z : R, x ## y -> ((x ## z) \/ (y ## z)).

meta.yml

@@ -54,6 +54,7 @@ supported_coq_versions:
 
 tested_coq_opam_versions:
 - version: 'dev'
+- version: '8.20'
 - version: '8.19'
 - version: '8.18'
 - version: '8.17'