Now compiles with 8.5 beta 3.

README

-PREREQUISITES
--------------
-
-This version is known to compile with:
-
- - Coq 8.4pl5
- - SCons 2.0
- - Ocaml 4.01.0
- - GNU C preprocessor 4.7
- 
-BUILDING INSTRUCTIONS
----------------------
-
-Say "scons" to build the full library, or "scons some_module.vo" to just 
-build some_module.vo (and its dependencies).
-
-In addition to common Make options like -j N and -k, SCons supports some 
-useful options of its own, such as --debug=time, which displays the time 
-spent executing individual build commands.
-
-scons -c replaces Make clean
-

theories/fin_maps.v

@@ -656,7 +656,7 @@ Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
 Proof.
   intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm.
   { destruct Hemp; eauto using map_to_list_empty_inv. }
-  exists i x. rewrite <-elem_of_map_to_list, Hm. by left.
+  exists i, x. rewrite <-elem_of_map_to_list, Hm. by left.
 Qed.
 
 (** Properties of the imap function *)
@@ -777,7 +777,7 @@ Proof.
   split; [|intros (i&x&?&?) Hm; specialize (Hm i x); tauto].
   rewrite map_Forall_to_list. intros Hm.
   apply (not_Forall_Exists _), Exists_exists in Hm.
-  destruct Hm as ([i x]&?&?). exists i x. by rewrite <-elem_of_map_to_list.
+  destruct Hm as ([i x]&?&?). exists i, x. by rewrite <-elem_of_map_to_list.
 Qed.
 End map_Forall.
 

theories/hashset.v

@@ -85,7 +85,7 @@ Proof.
       rewrite elem_of_list_intersection in Hx; naive_solver. }
     intros [(l&?&?) (k&?&?)]. assert (x ∈ list_intersection l k)
       by (by rewrite elem_of_list_intersection).
-    exists (list_intersection l k); split; [exists l k|]; split_ands; auto.
+    exists (list_intersection l k); split; [exists l, k|]; split_ands; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
   * unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
     intros [m1 ?] [m2 ?] x; simpl.
@@ -95,7 +95,7 @@ Proof.
     intros [(l&?&?) Hm2]; destruct (m2 !! hash x) as [k|] eqn:?; eauto.
     destruct (decide (x ∈ k)); [destruct Hm2; eauto|].
     assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference).
-    exists (list_difference l k); split; [right; exists l k|]; split_ands; auto.
+    exists (list_difference l k); split; [right; exists l,k|]; split_ands; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
   * unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
     intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split.

theories/list.v

@@ -487,8 +487,8 @@ Lemma list_lookup_other l i x :
   length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y.
 Proof.
   intros. destruct i, l as [|x0 [|x1 l]]; simplify_equality'.
-  * by exists 1 x1.
-  * by exists 0 x0.
+  * by exists 1, x1.
+  * by exists 0, x0.
 Qed.
 Lemma alter_app_l f l1 l2 i :
   i < length l1 → alter f i (l1 ++ l2) = alter f i l1 ++ l2.
@@ -604,7 +604,7 @@ Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
 Lemma elem_of_list_split l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
 Proof.
   induction 1 as [x l|x y l ? [l1 [l2 ->]]]; [by eexists [], l|].
-  by exists (y :: l1) l2.
+  by exists (y :: l1), l2.
 Qed.
 Lemma elem_of_list_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x.
 Proof.
@@ -1621,7 +1621,7 @@ Proof.
   split.
   * intros Hlk. induction k as [|y k IH]; inversion Hlk.
     + eexists [], k. by repeat constructor.
-    + destruct IH as (k1&k2&->&?); auto. by exists (y :: k1) k2.
+    + destruct IH as (k1&k2&->&?); auto. by exists (y :: k1), k2.
   * intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
 Qed.
 Lemma sublist_app_r l k1 k2 :
@@ -1633,9 +1633,9 @@ Proof.
     { eexists [], l. by repeat constructor. }
     rewrite sublist_cons_r. intros [?|(l' & ? &?)]; subst.
     + destruct (IH l k2) as (l1&l2&?&?&?); trivial; subst.
-      exists l1 l2. auto using sublist_cons.
+      exists l1, l2. auto using sublist_cons.
     + destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst.
-      exists (y :: l1) l2. auto using sublist_skip.
+      exists (y :: l1), l2. auto using sublist_skip.
   * intros (?&?&?&?&?); subst. auto using sublist_app.
 Qed.
 Lemma sublist_app_l l1 l2 k :
@@ -1647,7 +1647,7 @@ Proof.
     { eexists [], k. by repeat constructor. }
     rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst.
     destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst.
-    exists (k1 ++ x :: h1) h2. rewrite <-(associative_L (++)).
+    exists (k1 ++ x :: h1), h2. rewrite <-(associative_L (++)).
     auto using sublist_inserts_l, sublist_skip.
   * intros (?&?&?&?&?); subst. auto using sublist_app.
 Qed.
@@ -1865,7 +1865,7 @@ Proof.
   split.
   * rewrite contains_sublist_r. intros (l'&E&Hl').
     rewrite sublist_app_r in Hl'. destruct Hl' as (l1&l2&?&?&?); subst.
-    exists l1 l2. eauto using sublist_contains.
+    exists l1, l2. eauto using sublist_contains.
   * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
 Qed.
 Lemma contains_app_l l1 l2 k :
@@ -1875,7 +1875,7 @@ Proof.
   split.
   * rewrite contains_sublist_l. intros (l'&Hl'&E).
     rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst.
-    exists k1 k2. split. done. eauto using sublist_contains.
+    exists k1, k2. split. done. eauto using sublist_contains.
   * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
 Qed.
 Lemma contains_app_inv_l l1 l2 k :
@@ -2578,7 +2578,7 @@ Section fmap.
   Proof.
     revert l. induction k1 as [|y k1 IH]; simpl; [intros l ?; by eexists [],l|].
     intros [|x l] ?; simplify_equality'.
-    destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1) l2.
+    destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1), l2.
   Qed.
   Lemma fmap_length l : length (f <$> l) = length l.
   Proof. by induction l; f_equal'. Qed.
@@ -3006,7 +3006,7 @@ Section zip_with.
     { intros l k ?. by eexists [], [], l, k. }
     intros [|x l] [|y k] ?; simplify_equality'.
     destruct (IH l k) as (l1&k1&l2&k2&->&->&->&->&?); [done |].
-    exists (x :: l1) (y :: k1) l2 k2; simpl; auto with congruence.
+    exists (x :: l1), (y :: k1), l2, k2; simpl; auto with congruence.
   Qed.
   Lemma zip_with_inj `{!Injective2 (=) (=) (=) f} l1 l2 k1 k2 :
     length l1 = length k1 → length l2 = length k2 →

theories/natmap.v

@@ -19,7 +19,7 @@ Lemma natmap_wf_lookup {A} (l : natmap_raw A) :
 Proof.
   intros Hwf Hl. induction l as [|[x|] l IH]; simpl; [done| |].
   { exists 0. simpl. eauto. }
-  destruct IH as (i&x&?); eauto using natmap_wf_inv; [|by exists (S i) x].
+  destruct IH as (i&x&?); eauto using natmap_wf_inv; [|by exists (S i), x].
   intros ->. by destruct Hwf.
 Qed.
 

theories/pmap.v

@@ -114,9 +114,9 @@ Proof. by destruct i. Qed.
 Lemma Pmap_ne_lookup {A} (t : Pmap_raw A) : Pmap_ne t → ∃ i x, t !! i = Some x.
 Proof.
   induction 1 as [? x ?| l r ? IHl | l r ? IHr].
-  * intros. by exists 1 x.
-  * destruct IHl as [i [x ?]]. by exists (i~0) x.
-  * destruct IHr as [i [x ?]]. by exists (i~1) x.
+  * intros. by exists 1, x.
+  * destruct IHl as [i [x ?]]. by exists (i~0), x.
+  * destruct IHr as [i [x ?]]. by exists (i~1), x.
 Qed.
 
 Lemma Pmap_wf_eq_get {A} (t1 t2 : Pmap_raw A) :