`Control`#

Ltac2.Control

Generic backtracking control#

val throw : iexn -> 'a Proofview.tactic

Fatal exception throwing. This does not induce backtracking.

val zero : iexn -> 'a Proofview.tactic

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

val plus :
  'a Proofview.tactic ->
  (iexn -> 'a Proofview.tactic) ->
  'a Proofview.tactic

Backtracking point.

val once : 'a Proofview.tactic -> 'a Proofview.tactic

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.

val case : 'a Proofview.tactic -> 'a Proofview.case Proofview.tactic

case is the most general primitive to control backtracking:

If t would fail with e, case t returns Fail e.
If t would succeed and evaluate to v, then case t returns Next (v, h), where h is the continuation to execute in case of subsequent failure. Calling h resets the backtrackable state to its value when case was called.

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).

Proof state manipulation#

val numgoals : int Proofview.tactic

numgoals returns the number of goals currently focused.

val dispatch : unit Proofview.tactic list -> unit Proofview.tactic

dispatch 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).

Fails when the length of the tactic list is not equal to the number of focused goals.

val extend :
  unit Proofview.tactic list ->
  unit Proofview.tactic ->
  unit Proofview.tactic list ->
  unit Proofview.tactic

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 e r 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.

Fails if length b + length r is greater than the number of goals under focus.

val enter : unit Proofview.tactic -> unit Proofview.tactic

enter t applies t in each goal under focus independently.

val focus : int -> int -> 'a Proofview.tactic -> 'a Proofview.tactic

focus i j t 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 t. When focus returns, the present focus is restored.

If the range i–j is invalid, fails with a backtrackable "no such goal" error.

val shelve : unit Proofview.tactic

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

val shelve_unifiable : unit Proofview.tactic

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

val unshelve : 'a Proofview.tactic -> 'a Proofview.tactic

unshelve t runs t and unshelves existential variables added to the shelf by its execution, prepending them to the current goal. Returns the value produced by t.

val new_goal : evar -> unit Proofview.tactic

Adds the given evar to the list of goals as the last one. If it is already defined in the current state, does nothing.

Panics if the evar is not in the current state.

val reorder_goals : int list -> unit Proofview.tactic

reorder_goals l reorders the goals according to (1-indexed) list l: goal i after executing the tactic was goal nth l (i-1) before executing the tactic.

Raises if l is not a permutation of ints from 1 to numgoals.

val cycle : int -> unit Proofview.tactic

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

val progress : 'a Proofview.tactic -> 'a Proofview.tactic

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

Goal inspection#

val goal : constr Proofview.tactic

goal returns the conclusion of this goal.

Fails if there is not exactly one goal under focus.

val hyp : Environ.env -> Names.variable -> constr

hyp env id looks for the hypothesis or section variable in env with the given name.

raises Not_found
If the hypothesis could not be found in the environment.

val hyp_value : Environ.env -> Names.variable -> constr option

hyp_value env id looks for the hypothesis or section variable with the given name in env and returns its value (v in H := v) if there is one.

raises Not_found
If the hypothesis could not be found in the environment.

val hyps : Environ.env -> (Names.variable * constr option * constr) list

hyps env returns the list of hypotheses and section variables in the environment env.

Evars#

val with_holes :
  'a Proofview.tactic ->
  ('a -> 'b Proofview.tactic) ->
  'b Proofview.tactic

with_holes t f evaluates t, then applies f to the result, and fails if some evar generated by t has not been solved when f returns.

Timing#

val time : ?name:string -> 'a Proofview.tactic -> 'a Proofview.tactic

Displays the time taken by a tactic to evaluate.

val timeout : int -> 'a Proofview.tactic -> 'a Proofview.tactic

timeout n t runs t with a timeout of n seconds.

val timeoutf : float -> 'a Proofview.tactic -> 'a Proofview.tactic

timeoutf f t runs t with a timeout of f seconds.

Misc#

val abstract : ?name:ident -> unit Proofview.tactic -> unit Proofview.tactic

Abstract a subgoal.

val check_interrupt : unit Proofview.tactic

For internal use.

val print_err : err -> message

Print internal error.

Control#