diff options
| author | Théo Zimmermann | 2019-06-19 10:41:09 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-19 10:41:09 +0200 |
| commit | cdba5f7ceee1adfbdd96ffc82115fbc1e6750b80 (patch) | |
| tree | e4e94c235b18bdf96b82db071da74535ccd827c5 /doc | |
| parent | 415e83efb9e767ddf65b8c27d4e497592fd61f2c (diff) | |
| parent | 459b5ce5b2b825db43d645357f83d7fe17289bc5 (diff) | |
Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
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 |