Fix ListUtil for Coq 8.4

1 files changed, 19 insertions, 6 deletions

diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index d1e7bbd41..2dd1ce6b5 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -9,14 +9,14 @@ Proof. apply Min.min_case_strong; omega. Qed.
 Lemma max_def {x y} : max x y = x + (y - x).
 Proof. apply Max.max_case_strong; omega. Qed.
 Ltac coq_omega := omega.
-Ltac handle_min_max_for_omega :=
+Ltac handle_min_max_for_omega_gen min max :=
   repeat match goal with
-         | [ H : context[min _ _] |- _ ] => rewrite !min_def in H
-         | [ H : context[max _ _] |- _ ] => rewrite !max_def in H
-         | [ |- context[min _ _] ] => rewrite !min_def
-         | [ |- context[max _ _] ] => rewrite !max_def
+         | [ H : context[min _ _] |- _ ] => rewrite !min_def in H || setoid_rewrite min_def in H
+         | [ H : context[max _ _] |- _ ] => rewrite !max_def in H || setoid_rewrite max_def in H
+         | [ |- context[min _ _] ] => rewrite !min_def || setoid_rewrite min_def
+         | [ |- context[max _ _] ] => rewrite !max_def || setoid_rewrite max_def
          end.
-Ltac handle_min_max_for_omega_case :=
+Ltac handle_min_max_for_omega_case_gen min max :=
   repeat match goal with
          | [ H : context[min _ _] |- _ ] => revert H
          | [ H : context[max _ _] |- _ ] => revert H
@@ -24,11 +24,24 @@ Ltac handle_min_max_for_omega_case :=
          | [ |- context[max _ _] ] => apply Max.max_case_strong
          end;
   intros.
+Ltac handle_min_max_for_omega := handle_min_max_for_omega_gen min max.
+Ltac handle_min_max_for_omega_case := handle_min_max_for_omega_case_gen min max.
+(* In 8.4, Nat.min is a definition, so we need to unfold it *)
+Ltac handle_min_max_for_omega_compat_84 :=
+  let min := (eval cbv [min] in min) in
+  let max := (eval cbv [max] in max) in
+  handle_min_max_for_omega_gen min max.
+Ltac handle_min_max_for_omega_case_compat_84 :=
+  let min := (eval cbv [min] in min) in
+  let max := (eval cbv [max] in max) in
+  handle_min_max_for_omega_case_gen min max.
 Ltac omega_with_min_max :=
   handle_min_max_for_omega;
+  try handle_min_max_for_omega_compat_84;
   omega.
 Ltac omega_with_min_max_case :=
   handle_min_max_for_omega_case;
+  try handle_min_max_for_omega_case_compat_84;
   omega.
 Tactic Notation "omega" := coq_omega.
 Tactic Notation "omega" "*" := omega_with_min_max_case.