From 7e2f953c3c19904616c43990fada92e762aadec9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Jun 2010 08:27:03 +0000
Subject: Made tclABSTRACT normalize evars before saying it does not support
 them. This was the cause of the failure of compilation of CyclicAxioms after
 "replace" starting supporting open constrs (r13206).

Seized the opportunity to clean a little bit things around nf_evar,
whd_evar, check_evars, etc.

Removed obsolete printer mod_self_id from dev/db.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/db              | 2 --
 dev/doc/changes.txt | 5 +++++
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/db b/dev/db
index ca5c27de3b..6be2c20b92 100644
--- a/dev/db
+++ b/dev/db
@@ -6,8 +6,6 @@ install_printer Top_printers.ppidset
 install_printer Top_printers.ppevarsubst
 install_printer Top_printers.ppintset
 install_printer Top_printers.pplab
-install_printer Top_printers.ppmsid
-install_printer Top_printers.ppmbid
 install_printer Top_printers.ppdir
 install_printer Top_printers.ppmp
 install_printer Top_printers.ppkn
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 784283358a..1321b49785 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -17,6 +17,11 @@ generally fewer than the defined ones.
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
+** Light cleaning in evarutil.ml **
+
+whd_castappevar is now whd_head_evar
+obsolete whd_ise disappears
+
 ** Semantical change of h_induction_destruct **
 
 Warning, the order of the isrec and evar_flag was inconsistent and has
-- 
cgit v1.2.3