From 5ea3d1b1e01f56573e72d7818a4b7e6393ffdfa8 Mon Sep 17 00:00:00 2001
From: Théo Winterhalter
Date: Wed, 26 Sep 2018 11:26:50 +0200
Subject: Combined Scheme tests sort to use either "*" or "/\"

And update documentation.---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

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
 
-- 
cgit v1.2.3