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 05ecee1 commit f58f5adCopy full SHA for f58f5ad
Changelog.md
@@ -1,3 +1,15 @@
1
+# [3.2.0] 19/09/2025
2
+
3
+Requires Elpi 3.0.0 and Coq 8.20 or Rocq 9.0 or Rocq 9.1.
4
5
+### Apps:
6
+- Derive:
7
+ - Change `Set Uniform Inductive Parameters` is `#[export]` and not `#[global]`
8
9
+### API
10
+- Fix `.glob` generation for `coq.notation.*`
11
+- Fix binder handling in `coq.ltac.collect-goals`
12
13
# [3.1.0] 01/09/2025
14
15
Requires Elpi 3.0.0 and Coq 8.20 or Rocq 9.0 or Rocq 9.1.
0 commit comments