diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9cf819add53467f139305073b5601d1f22942fb7..693f04f1df1f286f15d3aa25e7683d1892ee3838 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,8 +30,8 @@ New features:
 - A `size` function for finite maps and prove some properties.
 - More results about `Qp` fractions.
 - More miscellaneous results about sets, maps, lists, multisets.
-- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `NoBackTrack` and
-  `tc_to_bool`.
+- Various type class utilities, e.g. `TCEq`, `TCIf`, `TCDiag`, `TCNoBackTrack`,
+  and `tc_to_bool`.
 - Generalize `gset_to_propset` to `set_to_propset` for any `SemiSet`.
 
 Changes:
diff --git a/theories/base.v b/theories/base.v
index f4a76923809bc90be5bd7d5230346410ed2106fb..64ccf58b61761628720da54f7636e80d86773afc 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -48,7 +48,7 @@ Arguments unseal {_ _} _ : assert.
 Arguments seal_eq {_ _} _ : assert.
 
 (** * Non-backtracking type classes *)
-(** The type class [NoBackTrack P] can be used to establish [P] without ever
+(** The type class [TCNoBackTrack P] can be used to establish [P] without ever
 backtracking on the instance of [P] that has been found. Backtracking may
 normally happen when [P] contains evars that could be instanciated in different
 ways depending on which instance is picked, and type class search somewhere else
@@ -60,8 +60,8 @@ issue #6714.
 
 See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
 of this type class. *)
-Class NoBackTrack (P : Prop) := { no_backtrack : P }.
-Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances.
+Class TCNoBackTrack (P : Prop) := { tc_no_backtrack : P }.
+Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
 
 (* A conditional at the type class level. Note that [TCIf P Q R] is not the same
 as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
diff --git a/theories/nat_cancel.v b/theories/nat_cancel.v
index 23028c93ea29e1267d308c0b69b6886dbf7d6ae3..d6dff3ace763e93eca963d36bc3609114bfb7bea 100644
--- a/theories/nat_cancel.v
+++ b/theories/nat_cancel.v
@@ -54,7 +54,7 @@ Module nat_cancel.
 
   we wrap the entire canceler in the [NoBackTrack] class. *)
   Instance nat_cancel_start m n m' n' :
-    NoBackTrack (NatCancelL m n m' n') → NatCancel m n m' n'.
+    TCNoBackTrack (NatCancelL m n m' n') → NatCancel m n m' n'.
   Proof. by intros [?]. Qed.
 
   Class MakeNatS (n1 n2 m : nat) := make_nat_S : m = n1 + n2.