From e1e750683d52e7d2b63a707b62c4d2af0e01a532 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 7 May 2014 16:19:24 +0200
Subject: Isolating a function "make_abstraction", new name of
 "letin_abstract", which compute an abstraction of the goal over a term or a
 pattern.

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

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 8a2b13ebee..d4e42142bb 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -75,7 +75,8 @@
       check_evars_are_solved explicitly to check that evars are solved.
   See also the corresponding commit log.
 
-- Tactics API: new_induct -> induction; new_destruct -> destruct
+- Tactics API: new_induct -> induction; new_destruct -> destruct;
+  letin_pat_tac do not accept a type anymore
 
 =========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
-- 
cgit v1.2.3