aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 8651c8e23a..f6c3985ba7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -164,6 +164,8 @@ Vernacular Commands
scope. If you want the previous behavior, use `Global Set SsrHave
NoTCResolution`.
- Multiple sections with the same name are allowed.
+- Combined Scheme can now work when inductive schemes are generated in sort
+ Type. It used to be limited to sort Prop.
Coq binaries and process model