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/doc/changes.txt | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'dev/doc') 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