From 971eca98f42917b719fb0c459d3ee0721ca1395f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Jul 2010 21:05:51 +0000
Subject: Cleaned a bit the grammar and terminology for binders (see
 dev/doc/changes.txt).

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

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 1321b49785..4617f4dee4 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -22,6 +22,13 @@ generally fewer than the defined ones.
 whd_castappevar is now whd_head_evar
 obsolete whd_ise disappears
 
+** Restructuration of the syntax of binders **
+
+binders_let -> binders
+binders_let_fixannot -> binders_fixannot
+binder_let -> closed_binder (and now covers only bracketed binders)
+binder was already obsolete and has been removed
+
 ** Semantical change of h_induction_destruct **
 
 Warning, the order of the isrec and evar_flag was inconsistent and has
-- 
cgit v1.2.3