Skip to content
Snippets Groups Projects

Add tactic `tc_solve`.

Merged Add tactic `tc_solve`.
robbert/tc_solve into master
1 unresolved thread
Merged Robbert Krebbers requested to merge robbert/tc_solve into master
1 unresolved thread

This is iSolveTC from Iris. I think it's good to move this tactic to std++ because it is not specific to Iris.

Also I used the tc_ prefix to be consistent with other type class related utilities in std++.

Merge request reports

Merge request pipeline #74696 passed

Stage: build

Merge request pipeline passed for efa1b8f0

Approval is optional
Ready to merge by members who can write to the target branch.

Merge details

  • 1 commit and 1 merge commit will be added to master (squashes 7 commits).
  • Source branch will be deleted.

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
stdpp/base.v
62 (** * Solving type class instances *)
63 (** The tactic [tc_solve] is used to solve type class goals by invoking type
64 class search. It is similar to [apply _], but it is more robust since it does
65 not affect unrelated goals/evars due to https://github.com/coq/coq/issues/6583.
66
67 The tactic [tc_solve] is particularly useful when building custom tactics that
68 need tight control over when type class search is invoked. In Iris, many of the
69 proof mode tactics make use of [notypeclasses refine] and use [tc_solve] to
70 manually invoke type class search.
71
72 Note that [typeclasses eauto] is multi-success. That means, whenever subsequent
73 tactics fail, it will backtrack to [typeclasses eauto] to try the next type
74 class instance. This is almost always undesired and can lead to poor performance
75 and horrible error messages. Hence, we wrap it in a [once]. *)
76 Ltac tc_solve :=
77 solve [once (typeclasses eauto)].
Please register or sign in to reply