Skip to content
Snippets Groups Projects
Commit d4458085 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/tc_solve' into 'master'

Add tactic `tc_solve`.

See merge request !425
parents d40a9005 efa1b8f0
Branches
Tags
1 merge request!425Add tactic `tc_solve`.
Pipeline #74697 passed
......@@ -7,6 +7,7 @@ API-breaking change is listed.
`difference_difference_L` -> `difference_difference_l_L`, add
`difference_difference_r` and `difference_difference_r_L`.
- Let `set_solver` use `eauto` (instead of `idtac`) as its default solver.
- Add tactic `tc_solve` (this was `iSolveTC` in Iris).
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
......@@ -59,6 +59,23 @@ End seal.
Global Arguments unseal {_ _} _ : assert.
Global Arguments seal_eq {_ _} _ : assert.
(** * Solving type class instances *)
(** The tactic [tc_solve] is used to solve type class goals by invoking type
class search. It is similar to [apply _], but it is more robust since it does
not affect unrelated goals/evars due to https://github.com/coq/coq/issues/6583.
The tactic [tc_solve] is particularly useful when building custom tactics that
need tight control over when type class search is invoked. In Iris, many of the
proof mode tactics make use of [notypeclasses refine] and use [tc_solve] to
manually invoke type class search.
Note that [typeclasses eauto] is multi-success. That means, whenever subsequent
tactics fail, it will backtrack to [typeclasses eauto] to try the next type
class instance. This is almost always undesired and can lead to poor performance
and horrible error messages. Hence, we wrap it in a [once]. *)
Ltac tc_solve :=
solve [once (typeclasses eauto)].
(** * Non-backtracking type classes *)
(** 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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment