From 2194292dbe88674fd9a606bb22f28d332f670f77 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jun 2016 23:24:57 +0200
Subject: Revise syntax of Hint Cut

As noticed by C. Cohen it was confusingly different from standard
notation.
---
 doc/refman/RefMan-tac.tex | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 527226f687..89b8107ed7 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{)} & 
-- 
cgit v1.2.3