diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-09 23:24:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | 2194292dbe88674fd9a606bb22f28d332f670f77 (patch) | |
| tree | 21c2e91b13a5de21856554b17f5dfaa61101e253 /doc | |
| parent | af7a9a4e44739968b68aeb1cb0a1f70a1aa34e88 (diff) | |
Revise syntax of Hint Cut
As noticed by C. Cohen it was confusingly different from standard
notation.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 527226f68..89b8107ed 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3836,13 +3836,15 @@ Abort. This command can be used to cut the proof-search tree according to a regular expression matching paths to be cut. The grammar for regular - expressions is the following: + expressions is the following. Beware, there is no operator precedence + during parsing, one can check with \texttt{Print HintDb} to verify the + current cut expression: \[\begin{array}{lcll} e & ::= & \ident & \text{ hint or instance identifier } \\ - & & \texttt{*} & \text{ any hint } \\ + & & \texttt{\_} & \text{ any hint } \\ & & e | e' & \text{ disjunction } \\ - & & e ; e' & \text{ sequence } \\ - & & ! e & \text{ Kleene star } \\ + & & e e' & \text{ sequence } \\ + & & e * & \text{ Kleene star } \\ & & \texttt{emp} & \text{ empty } \\ & & \texttt{eps} & \text{ epsilon } \\ & & \texttt{(} e \texttt{)} & |