Library Ltac2.Control

Panic

Fatal exception throwing. This does not induce backtracking. Generic backtracking control

zero e raises the exception e, passing control to the current backtracking continuation.

Backtracking point, cf Backtracking section of the ltac2 refman.

once t behaves like t, except it has at most one success: once t stops after the first success of t. If t fails with e, once t also fails with e. If once t; t' fails on t', then once t will not backtrack and evaluate t for another value, and will instead fail.

case is the most general primitive to control backtracking:

• If t () would fail with e, case t returns Err e.
• If t () would succeed and evaluate to v then case t returns Val (v, h), where h is the continuation to execute in case of subsequent failure. case reifies a backtracking computation into an inspectable value, it allows the programmer to make explicit the effects which are normally implicit (i.e., they do not appear in the type system).

once_plus run handle is once applied to plus run handle. Proof state manipulation

Return the number of goals currently focused.

The dispatch tactical is used to apply a different tactic to each goal under focus. It works by applying each of the tactics in a focus restricted to the corresponding goal (starting with the first goal). When the length of the tactic list is not equal to the number of focused goals, raises Internal err.

extend is a more flexible variant of dispatch, where the second argument tactic is "repeated" enough times such that every goal has a tactic assigned to it. extend b r e applies the tactics in b to the first length b goals, the tactics in r to the last length r goals, and e to all tactics in between. Raises Internal err if length b + length r is greater than the number of goals under focus.

enter takes a single tactic t and applies t in each goal under focus independently.

focus i j tac focuses a proofview on the goals from index i to index j (inclusive, goals are indexed from 1) and runs t with those goals under focus, i.e. goals number i to j become the only focused goals during the execution of tac. When focus returns, the present focus is restored. If the range i - j is invalid, fails with a backtrackable "no such goal" error.

If n is positive, cycle n puts the n first goal last. If n is negative, then it puts the n last goals first.

Shelve all goals under focus. The goals are placed on the shelf for later use, or to be solved by side-effects.

Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not considered).

Adds the given evar to the list of goals as the last one. If it is already defined in the current state, don't do anything. Panics if the evar is not in the current state.

Runs the closure, then unshelves existential variables added to the shelf by its execution, prepending them to the current goal. Returns the value produced by the closure.

progress t checks the state of the proof after t. It it is identical to the state before, then progress t fails, otherwise it succeeds like t. Goal inspection

Panics if there is not exactly one goal under focus. Otherwise returns the conclusion of this goal.

Panics if there is more than one goal under focus. If there is no goal under focus, looks for the section variable with the given name. If there is one, looks for the hypothesis with the given name.

Panics if there is more than one goal under focus. If there is no goal under focus, looks for the section variable with the given name and return its value ("v" in "H := v") if there is one. If there is one, looks for the hypothesis with the given name and return its value if there is one.

Panics if there is more than one goal under focus. If there is no goal under focus, returns the list of section variables. If there is one, returns the list of hypotheses. In both cases, the list is ordered with rightmost values being last introduced. Refinement

refine t computes the type of the term t () and unifies the type with the current goal. All unification variables produced while computing t () not solved by this unification process are added as new goals. Evars

with_holes x f evaluates x, then apply f to the result, and fails if all evars generated by the call to x have not been solved when f returns. Misc

Displays the time taken by a tactic to evaluate.

Abstract a subgoal.

For internal use. Assertions throwing exceptions and short form throws

Short form backtracks

Backtraces. throw_bt info e is similar to throw e, but raises e with the backtrace represented by info.

zero_bt info e is similar to zero e, but raises e with the backtrace represented by info.

plus_bt run handle is similar to plus run handle (up to the type missmatch for handle), but it calls handle with an extra argument representing the backtrace at the point of the exception. The handle function can thus decide to re-attach that backtrace when using the throw_bt or zero_bt functions.

once_plus_bt run handle is a non-backtracking variant of once_plus that has backtrace support similar to that of plus_bt.

Timeout. timeout t thunk calls thunk () with a timeout of t seconds.

timeoutf t thunk calls thunk () with a timeout of t seconds.