From 8c23671d5a8bf6a5c197bbcaec1af2084d654ed3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 18 Apr 2007 08:59:42 +0000
Subject: - Correction d'un bug de make_clenv_binding_apply révélé par le
 commit 9771   (les let-in étaient comptés comme des produits, introduisant
 une incohérence   sur le nombre de produits à instancier dans les lemmes
 appelés par apply). - Export simplest_eapply pour utilisation dans
 Sophia/RecursiveDefinition. - Doc développeur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9785 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/changes.txt | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 90e2949681..ad5704db8e 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,3 +1,15 @@
+=========================================
+= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
+=========================================
+
+A few differences in Coq ML interfaces between Coq V8.0 and V8.1
+================================================================
+
+** Functions
+
+Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
+
+
 =========================================
 = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
 =========================================
-- 
cgit v1.2.3