aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorherbelin2008-06-11 11:25:07 +0000
committerherbelin2008-06-11 11:25:07 +0000
commit1d67eb8a50a6d4f185aead5a23442e4b91270594 (patch)
tree57e6635ae182429317cf6e81fb9f25c85aaa915d /dev
parentba61b1c136505c901c23f6a83cae6d29cedcd96c (diff)
MAJ diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11102 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.txt7
1 files changed, 6 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index d8cdf738d9..b7545e09c0 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,9 +2,14 @@
= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
=========================================
-A few differences in Coq ML interfaces between Coq V8.0 and V8.1
+A few differences in Coq ML interfaces between Coq V8.1 and V8.2
================================================================
+** Datatypes
+
+List of occurrences moved from "int list" to "Termops.occurrences" (an
+alias to "bool * int list").
+
** Functions
Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply