From c43d5e8682457868e7af1a65b25cec6d344eee8c Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 14 Jul 2024 18:37:21 +0200 Subject: [PATCH 1/2] backwards-compatible fix of recent deprecation of auto using term --- Cut.v | 2 +- MinMax.v | 20 ++++++++++---------- Order.v | 4 ++-- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Cut.v b/Cut.v index cdc2219..813723d 100644 --- a/Cut.v +++ b/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. diff --git a/MinMax.v b/MinMax.v index f1930bf..cf454b4 100644 --- a/MinMax.v +++ b/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)). diff --git a/Order.v b/Order.v index 6a5d482..6310588 100644 --- a/Order.v +++ b/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)). From 52b68ad4a0e05799431a12c1b159df8f86776c88 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 14 Jul 2024 18:37:38 +0200 Subject: [PATCH 2/2] test Coq 8.20 in ci --- .github/workflows/docker-action.yml | 1 + meta.yml | 1 + 2 files changed, 2 insertions(+) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index b58ddcc..1b15dff 100644 --- a/.github/workflows/docker-action.yml +++ b/.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' diff --git a/meta.yml b/meta.yml index 4fdc0c0..a2c957e 100644 --- a/meta.yml +++ b/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'