From e3027f8d8b880e153019a1358b3c876723e67633 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 27 Apr 2018 11:41:46 +0200
Subject: [PATCH] Get rid of fix/cofix without a name; these are deprecated in
 Coq 8.8.

---
 theories/countable.v | 4 ++--
 theories/numbers.v   | 8 ++++----
 theories/pretty.v    | 2 +-
 theories/relations.v | 2 +-
 theories/streams.v   | 6 +++---
 theories/stringmap.v | 2 +-
 6 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/theories/countable.v b/theories/countable.v
index 567903ad..9e3a47e5 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -348,11 +348,11 @@ Fixpoint gen_tree_of_list {T}
 Lemma gen_tree_of_to_list {T} k l (t : gen_tree T) :
   gen_tree_of_list k (gen_tree_to_list t ++ l) = gen_tree_of_list (t :: k) l.
 Proof.
-  revert t k l; fix 1; intros [|n ts] k l; simpl; auto.
+  revert t k l; fix FIX 1; intros [|n ts] k l; simpl; auto.
   trans (gen_tree_of_list (reverse ts ++ k) ([inl (length ts, n)] ++ l)).
   - rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l).
     induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
-    rewrite reverse_cons, <-!(assoc_L _), gen_tree_of_to_list; simpl; auto.
+    rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
   - simpl. by rewrite take_app_alt, drop_app_alt, reverse_involutive
       by (by rewrite reverse_length).
 Qed.
diff --git a/theories/numbers.v b/theories/numbers.v
index e80bb320..4be6c114 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -48,11 +48,11 @@ Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
 Proof.
   assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
     y = y' → eq_dep nat (le x) y p y' q) as aux.
-  { fix 3. intros x ? [|y p] ? [|y' q].
+  { fix FIX 3. intros x ? [|y p] ? [|y' q].
     - done.
-    - clear nat_le_pi. intros; exfalso; auto with lia.
-    - clear nat_le_pi. intros; exfalso; auto with lia.
-    - injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
+    - clear FIX. intros; exfalso; auto with lia.
+    - clear FIX. intros; exfalso; auto with lia.
+    - injection 1. intros Hy. by case (FIX x y p y' q Hy). }
   intros x y p q.
   by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
 Qed.
diff --git a/theories/pretty.v b/theories/pretty.v
index a26e574b..c879e43e 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -25,7 +25,7 @@ Proof. done. Qed.
 Lemma pretty_N_go_help_irrel x acc1 acc2 s :
   pretty_N_go_help x acc1 s = pretty_N_go_help x acc2 s.
 Proof.
-  revert x acc1 acc2 s; fix 2; intros x [acc1] [acc2] s; simpl.
+  revert x acc1 acc2 s; fix FIX 2; intros x [acc1] [acc2] s; simpl.
   destruct (decide (0 < x)%N); auto.
 Qed.
 Lemma pretty_N_go_step x s :
diff --git a/theories/relations.v b/theories/relations.v
index d9e65e5d..fa27e104 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -223,7 +223,7 @@ Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x)
       (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
     (x : A) (acc1 acc2 : Acc R x) :
   E _ (Fix_F B F acc1) (Fix_F B F acc2).
-Proof. revert x acc1 acc2. fix 2. intros x [acc1] [acc2]; simpl; auto. Qed.
+Proof. revert x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed.
 
 Lemma Fix_unfold_rel `{R: relation A} (wfR: wf R) (B: A → Type) (E: ∀ x, relation (B x))
       (F: ∀ x, (∀ y, R y x → B y) → B x)
diff --git a/theories/streams.v b/theories/streams.v
index 0a1be8b6..d4e610d5 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -41,9 +41,9 @@ Proof. by constructor. Qed.
 Global Instance equal_equivalence : Equivalence (≡@{stream A}).
 Proof.
   split.
-  - now cofix; intros [??]; constructor.
-  - now cofix; intros ?? [??]; constructor.
-  - cofix; intros ??? [??] [??]; constructor; etrans; eauto.
+  - now cofix FIX; intros [??]; constructor.
+  - now cofix FIX; intros ?? [??]; constructor.
+  - cofix FIX; intros ??? [??] [??]; constructor; etrans; eauto.
 Qed.
 Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).
 Proof. by constructor. Qed.
diff --git a/theories/stringmap.v b/theories/stringmap.v
index eb6871db..14fffc96 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -45,7 +45,7 @@ Lemma fresh_string_fresh {A} (m : stringmap A) s : m !! fresh_string s m = None.
 Proof.
   unfold fresh_string. destruct (m !! s) as [a|] eqn:Hs; [clear a Hs|done].
   generalize 0 (wf_guard 32 (fresh_string_R_wf s m) 0); revert m.
-  fix 3; intros m n [?]; simpl; unfold fresh_string_go at 1; simpl.
+  fix FIX 3; intros m n [?]; simpl; unfold fresh_string_go at 1; simpl.
   destruct (Some_dec (m !! _)) as [[??]|?]; auto.
 Qed.
 Definition fresh_string_of_set (s : string) (X : stringset) : string :=
-- 
GitLab