7.1 Syntax of tactics and tacticals

7.1 Syntax of tactics and tacticals

A tactic is applied as an ordinary command. If the tactic does not address the first subgoal, the command may be preceded by the wished subgoal number. See figure 7.1 for the syntax of tactic invocation and tacticals.




tactic ::= atomic_tactic
  | ( tactic )
  | tactic Orelse tactic
  | Repeat tactic
  | Do num tactic
  | Info tactic
  | Abstract tactic
  | Abstract tactic using ident
  | tactic ; tactic
  | tactic ;[ tactic | ...| tactic ]
tactic_invocation ::= num : tactic .
  | tactic .


Figure 7.1:Invocation of tactics and tacticals



Remarks:
  1. The infix tacticals Orelse and ``...; ...'' are associative. The tactical Orelse binds more than the prefix tacticals Try, Repeat, Do, Info and Abstract which themselves bind more than the postfix tactical ``...;[ ... ]'' which binds more than ``...; ...''.

    For instance

    Try Repeat tactic1 Orelse tactic2;tactic3;[tactic31|...|tactic3n);tactic4)

    is understood as

    (Try (Repeat (tactic1 Orelse tactic2))); ((tactic3;[tactic31|...|tactic3n]);tactic4).

  2. An atomic_tactic is any of the tactics listed below.


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.2.0.html at 8/10/98