diff options
| author | Hugo Herbelin | 2018-12-26 23:46:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-25 15:36:59 +0200 |
| commit | 7050ceaa09a29c3f50620a8d3f8439c3d69a10d0 (patch) | |
| tree | 274322620e33ad5b3a53c62d4c1f028f9077dd02 /doc | |
| parent | 5727443376480be4793757fd5507621ad4f09509 (diff) | |
Documenting syntax "injection ... as [= pat1 ... patn ]".
To prevent confusion, forbidding a mix of the "injection term as pat1
... patn" and of the "injection term as [= pat1 ... patn]" syntax: If
a "[= ...]" occurs, this should be a singleton list of patterns.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/09288-injection-as.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 19 |
2 files changed, 20 insertions, 3 deletions
diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst new file mode 100644 index 0000000000..6a74551f06 --- /dev/null +++ b/doc/changelog/04-tactics/09288-injection-as.rst @@ -0,0 +1,4 @@ +- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as + an alternative to :n:`injection @term as {+ @simple_intropattern}` using + the standard :n:`@injection_intropattern` syntax (`#09288 + <https://github.com/coq/coq/pull/09288>`_, by Hugo Herbelin). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 67d32835f5..fa6d62ffa2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -131,16 +131,17 @@ include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. simple_intropattern_closed : `naming_intropattern` : _ : `or_and_intropattern` - : `equality_intropattern` + : `rewriting_intropattern` + : `injection_intropattern` naming_intropattern : `ident` : ? : ?`ident` or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] : ( `simple_intropattern` , ... , `simple_intropattern` ) : ( `simple_intropattern` & ... & `simple_intropattern` ) - equality_intropattern : -> + rewriting_intropattern : -> : <- - : [= `intropattern_list` ] + injection_intropattern : [= `intropattern_list` ] or_and_intropattern_loc : `or_and_intropattern` : `ident` @@ -2285,6 +2286,18 @@ and an explanation of the underlying technique. to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. + .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern + injection @num as @injection_intropattern + injection as @injection_intropattern + einjection @term {? with @bindings_list} as @injection_intropattern + einjection @num as @injection_intropattern + einjection as @injection_intropattern + + These are equivalent to the previous variants but using instead the + syntax :token:`injection_intropattern` which :tacn:`intros` + uses. In particular :n:`as [= {+ @simple_intropattern}]` behaves + the same as :n:`as {+ @simple_intropattern}`. + .. flag:: Structural Injection This option ensure that :n:`injection @term` erases the original hypothesis |