From d9bb54508af81c02cc33454bb981da1641c9b337 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Sep 2020 13:18:31 +0200
Subject: [PATCH] remove Coq bug #12944 work-arounds

---
 theories/hashset.v | 3 +--
 theories/sorting.v | 3 +--
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/hashset.v b/theories/hashset.v
index 1ed944a9..065c58b1 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -104,8 +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 ?];
+    induction Hm as [|[n l] m' [??] Hm];
       csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
     apply NoDup_app; split_and?; eauto.
     setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
diff --git a/theories/sorting.v b/theories/sorting.v
index d405d4c0..11fada6e 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -180,8 +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;
+      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;
       constructor; eauto using HdRel_list_merge, HdRel_cons.
-- 
GitLab