From d95360254e71a5d428bfeb30b622b1b2ea8735c4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 30 Aug 2020 11:51:22 +0200
Subject: [PATCH] add FIXMEs for Coq bug work-arounds
---
theories/hashset.v | 1 +
theories/sorting.v | 1 +
2 files changed, 2 insertions(+)
diff --git a/theories/hashset.v b/theories/hashset.v
index 920b4949..1ed944a9 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -104,6 +104,7 @@ Proof.
intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list.
- unfold elements, hashset_elements. intros [m Hm]; simpl.
rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
+ (* FIXME: trailing [?] works around Coq bug #12944. *)
induction Hm as [|[n l] m' [??] Hm ?];
csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
apply NoDup_app; split_and?; eauto.
diff --git a/theories/sorting.v b/theories/sorting.v
index afdab495..d405d4c0 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -180,6 +180,7 @@ Section merge_sort_correct.
Sorted R l1 → Sorted R l2 → Sorted R (list_merge R l1 l2).
Proof.
intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
+ (* FIXME: trailing [?] works around Coq bug #12944. *)
induction 1 as [|x2 l2 IH2 ?]; rewrite ?list_merge_cons; simpl;
repeat case_decide;
repeat match goal with H : ¬R _ _ |- _ => apply total_not in H end;
--
GitLab