From ae135201cac7a65a29bbe251f25620edaf755a0d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Aug 2016 14:00:01 +0200
Subject: [PATCH] Better Coq 8.6 compatibility

With Coq 8.6, you can no longer have intro patterns that give more names than
the constructor has.  Also, patterns with too few names are now interpreted as
filling up with "?", rather than putting the unnamed parts into the goal again.

Furthermore, it seems the behavior of "simplify_eq/=" changed, I guess
hypotheses are considered in different order now.  I managed to work around
this, but it all seem kind of fragile.

The next compilation failure is an "Anyomaly: ... Please report", so that's what I will do.
---
 algebra/cofe_solver.v | 4 ++--
 prelude/collections.v | 2 +-
 prelude/list.v        | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 515028163..9c5c79f63 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -109,14 +109,14 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
 Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
   gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
 Proof.
-  assert (i = i2 + i1) by lia; simplify_eq/=. revert j x H1.
+  assert (i = i2 + i1) by lia; move:H1=>H1; simplify_eq/=. revert j x H1.
   induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
     [by rewrite coerce_id|by rewrite g_coerce IH].
 Qed.
 Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
   coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
 Proof.
-  assert (i = i1 + i2) by lia; simplify_eq/=.
+  assert (i = i1 + i2) by lia; move:H1=>H1; simplify_eq/=.
   induction i1 as [|i1 IH]; simplify_eq/=;
     [by rewrite coerce_id|by rewrite coerce_f IH].
 Qed.
diff --git a/prelude/collections.v b/prelude/collections.v
index 850226e15..ef7383d52 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -390,7 +390,7 @@ Section simple_collection.
     split.
     - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
       setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
-    - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
+    - intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |].
       intros. apply elem_of_union_r; auto.
   Qed.
 
diff --git a/prelude/list.v b/prelude/list.v
index 59b263318..9a384897e 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -926,7 +926,7 @@ Proof. by destruct n. Qed.
 Lemma drop_length l n : length (drop n l) = length l - n.
 Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
 Lemma drop_ge l n : length l ≤ n → drop n l = [].
-Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
+Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed.
 Lemma drop_all l : drop (length l) l = [].
 Proof. by apply drop_ge. Qed.
 Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
@@ -2828,7 +2828,7 @@ Section fmap.
     (∀ x, f x = y) → f <$> l = replicate (length l) y.
   Proof. intros; induction l; f_equal/=; auto. Qed.
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
-  Proof. revert i. induction l; by intros [|]. Qed.
+  Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
   Lemma list_lookup_fmap_inv l i x :
     (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
   Proof.
-- 
GitLab