Correctif Tactic Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8487 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 5 deletions

diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 281e082dd..12b41f36c 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -849,10 +849,10 @@ syntax
 {\tt ident} $|$
 {\tt simple\_intropattern} $|$
 {\tt hyp} \\ & $|$ &
-{\tt quantified\_hypothesis} $|$
+% {\tt quantified\_hypothesis} $|$
 {\tt reference} $|$
 {\tt constr} \\ & $|$ &
-{\tt castedopenonstr} $|$
+%{\tt castedopenconstr} $|$
 {\tt integer} \\ & $|$ &
 {\tt int\_or\_var} $|$
 {\tt tactic} $|$
@@ -879,11 +879,12 @@ Tactic argument type & parsed as & interpreted as & as in tactic \\
 {\tt\small ident} & identifier & a user-given name & {\tt intro} \\
 {\tt\small simple\_intropattern} & intro\_pattern & an intro\_pattern & {\tt intros}\\
 {\tt\small hyp} & identifier & an hypothesis defined in context & {\tt clear}\\
-{\tt\small quantified\_hypothesis} & identifier or integer & a named or non dep. hyp. of the goal & {\tt intros until}\\
+%% quantified_hypothesis actually not supported
+%%{\tt\small quantified\_hypothesis} & identifier or integer & a named or non dep. hyp. of the goal & {\tt intros until}\\
 {\tt\small reference} & qualified identifier & a global reference of term & {\tt unfold}\\
 {\tt\small constr} & term & a term & {\tt exact} \\
-{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\
-{\tt\small constr\_with\_bindings} & term with bindings & a term with bindings & {\tt apply}\\
+%% castedopenconstr actually not supported
+%%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\
 {\tt\small integer} & integer & an integer &  \\
 {\tt\small int\_or\_var} & identifier or integer & an integer & {\tt do} \\
 {\tt\small tactic} & tactic & a tactic & \\