Commit d9bb5450 authored by Ralf Jung's avatar Ralf Jung
Browse files

remove Coq bug #12944 work-arounds

parent 2277106c
......@@ -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 *.
......
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment