Skip to content
Snippets Groups Projects
Commit b2f88a5a authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

CHANGELOG improvements by Ralf.

parent 331f96f7
No related branches found
No related tags found
No related merge requests found
......@@ -144,13 +144,15 @@ Coq 8.13 is no longer supported.
classes, their results may have become more concise.
* Support n-ary versions of `iIntros`, `iRevert`, `iExists`, `iDestruct`, `iMod`,
`iFrame`, `iRevertIntros`, `iPoseProof`, `iInduction`, `iLöb`, `iInv`, and
`iAssert`. (by Jan-Oliver Kaiser, and Rodolphe Lepigre)
`iAssert`. (by Jan-Oliver Kaiser and Rodolphe Lepigre)
* Add tactics `ltac1_list_iter` and `ltac1_list_rev_iter` to iterate over
lists of `ident`s/`simple intropatterns`/`constr`/etc using Ltac1. To read how
lists of `ident`s/`simple intropatterns`/`constr`/etc using Ltac1. See
[iris/proofmode/base.v](proofmode/base.v) for documentation on how
to use these tactics to convert your own fixed arity tactics to an n-ary
variant, see [iris/proofmode/base.v](proofmode/base.v).
* The tactic `iIntros` will always call `iStartProof`, so even `iIntros (x)`. If
you do not want to start the proof mode, use ordinary `intros`.
variant.
* The tactic `iIntros` will always call `iStartProof`, even when there is no Iris
pattern such as in `iIntros (x)`. If you do not want to start the proof mode,
use ordinary `intros`.
**Changes in `base_logic`:**
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment