- Require coq-ext-lib >= 0.11.1
- Change precedence of
>>=
to level 58 (previously at level 50). - Add
tau_eutt
andtau_euttge
(the latter was actually renamed fromtau_eutt
).
-
Add compatibility with Coq 8.10 and 8.11
-
Require coq-ext-lib 0.10.3 (only this one version, not 0.10.2 or 0.11.0!) for notation compatibility.
-
Notation changes
-
Notation convention (from coq-ext-lib, PR 68): odd is right, even is left.
-
Change precedence of monad notations in
ITreeNotations
.x <- t1 ;; t2
,t1 ;; t2
,' p <- t1 ;; t2
,>=>
at level 61 (previously level 60).
-
Change precedence of notation
-<
at level 92 (previously level 90, but it is currently used by math-classes with right associativity). -
Remove notations
KTree.iter
andKTree.loop
(useiter (C := ktree _)
instead for example).
-
-
Add
pure_inl
,pure_inr
. -
Add
eutt_interp_state
andeutt_interp_state_eq
(the latter was actually renamed fromeutt_interp_state
).
The previous release was not that stable... Too many changes to count.
Version 2.0.0 corresponds to our POPL20 paper.
First stable release