We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 7b8230d commit 7c37d15Copy full SHA for 7c37d15
Changelog.md
@@ -9,6 +9,8 @@
9
- Change `coq.gref->path` and `coq.gref->id` do work on `gref` which point
10
to mutual inductives.
11
- New `coq.env.term-dependencies` computing all the `grefs` occurring in a term.
12
+ - New `coq.redflag` and `coq.redflags` types for `@redflags!` option understood
13
+ by `coq.reduction.lazy.*` `and coq.reduction.cbv.norm`
14
15
## [1.15.6] - 27-08-2022
16
0 commit comments