From 72d05b03d86f3b0672bdda8ffb3d403c2601223a Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 8 Sep 2014 09:54:58 +0200
Subject: CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].

---
 CHANGES | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index fc111d211d..6982b63ff7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,10 +35,13 @@ Logic
 
 Vernacular commands
 
+- A command "Variant" allows to define non-recursive variant types.
 - The command "Record foo ..." does not generate induction principles
-  (foo_rect, foo_rec, foo_ind) anymore by default (feature wish #2693).
-  A flag "Set/Unset Record Elimination Schemes" allows changing this.
-  The tactic "induction" on a record is now actually doing "destruct".
+  (foo_rect, foo_rec, foo_ind) anymore by default (feature wish
+  #2693). The command "Variant foo ..." does not either.  A flag
+  "Set/Unset Nonrecursive Elimination Schemes" allows changing this.
+  The tactic "induction" on a "Record" or a "Variant" is now actually
+  doing "destruct".
 - The "Open Scope" command can now be given also a delimiter (e.g. Z).
 - The "Definition" command now allows the "Local" modifier, allowing
   for non-importable definitions.
-- 
cgit v1.2.3