diff options
| author | Matthieu Sozeau | 2016-05-27 19:37:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 855143c550cad6694f77a782d1056b07f8197bd3 (patch) | |
| tree | 45ba61851044e31d4b3a8e2d1a0132e985656db9 /kernel/nativecode.mli | |
| parent | 9e6696d67c7613b665799f7fe7f1a35cf4daf4b3 (diff) | |
bteauto: a Proofview.tactic for multiple goals
Add an option to force backtracking at toplevel, which
is used by default when calling typeclasses eauto on a set of goals.
They might be depended on by other subgoals, so the tactic should
be backtracking by default, a once can make it not backtrack.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions