diff options
| author | Hugo Herbelin | 2019-05-24 20:53:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-16 20:58:50 +0200 |
| commit | 459b5ce5b2b825db43d645357f83d7fe17289bc5 (patch) | |
| tree | 45dd0a7a3d07bda0292c5f4bedd1b9e0bae858a1 /doc | |
| parent | 6eba5b5ba91f9ec02b809e0c223324e0f4fdbf85 (diff) | |
Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".
This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual
After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.
Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9b381cb9de..fd315c097d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1716,9 +1716,9 @@ Tactic notations allow to customize the syntax of tactics. They have the followi - intro * - ``simple_intropattern`` - - intro_pattern - - an intro pattern - - intros + - simple_intropattern + - an introduction pattern + - assert as * - ``hyp`` - identifier |