diff --git a/theories/countable.v b/theories/countable.v
index 567903ad8e945be3c9f851d2db19362a029781d1..9e3a47e51cb601dcc2c045b3316f61d41fdaeb2d 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 e80bb32032f61969e4e17a6828958a72729be19a..4be6c114086767c9e46dbadd0bbaf966a4a60225 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 a26e574b794112f9ba097590afb559625fb7ea27..c879e43e4bdeefb604eeb1febce0accf41bb9408 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 d9e65e5da1064d7d1f345e3a36e0a825a7e9b8ce..fa27e104c6c741ae2424f54505d0b1186d6b3d2d 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 0a1be8b6ea16a4566382ee7edaea6d7961c4403d..d4e610d50d3d266b8c0b0c9bc1fcf84e92538907 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 eb6871db9b48ec00f917ec422e7afe2c44e6d96e..14fffc9671751490e9d484267e0ac3202a18de78 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 :=