Commit 32eab16e authored by Robbert Krebbers's avatar Robbert Krebbers

Rename `NoBackTrack` into `TCNoBackTrack`.

parent b52e911c
Pipeline #16301 passed with stage
in 10 minutes and 26 seconds
......@@ -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:
......
......@@ -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
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment