From 32eab16e70a9ded5d2dfa56477f5c24d07c51070 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Apr 2019 10:43:49 +0200
Subject: [PATCH] Rename `NoBackTrack` into `TCNoBackTrack`.

---
 CHANGELOG.md          | 4 ++--
 theories/base.v       | 6 +++---
 theories/nat_cancel.v | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9cf819ad..693f04f1 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 f4a76923..64ccf58b 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 23028c93..d6dff3ac 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.
-- 
GitLab