From b6c3f54d04ce441ac68ffabfca69c18847707518 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Aug 2014 17:16:58 +0200
Subject: A reorganization of the "assert" tactics (hopefully uniform naming
 scheme, redundancies, possibility of chaining a tactic knowing the name of
 introduced hypothesis, new proof engine).

---
 dev/doc/changes.txt | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4ea33ddbea..cea4cf1224 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -91,6 +91,9 @@
   "intros_pattern" and "intros_patterns" is not anymore behaving like
   tactic "intros" on the empty list.
 
+- API of cut tactics changed: cut_intro should be replaced by
+  "enough_tac Anonymous"
+
 =========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
 =========================================
-- 
cgit v1.2.3