From 976c58f30f862cff979ec2f925ccbc0d995d5b77 Mon Sep 17 00:00:00 2001
From: Ralf Jung
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.
---
theories/collections.v | 2 +-
theories/list.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/collections.v b/theories/collections.v
index 6f4e526..3a49b8d 100644
--- a/theories/collections.v
+++ b/theories/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/theories/list.v b/theories/list.v
index 59b7bda..ab08c51 100644
--- a/theories/list.v
+++ b/theories/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