diff options
| author | herbelin | 2010-06-29 08:27:03 +0000 |
|---|---|---|
| committer | herbelin | 2010-06-29 08:27:03 +0000 |
| commit | 7e2f953c3c19904616c43990fada92e762aadec9 (patch) | |
| tree | 8268d6e2b66ccdcce69df129ed98703e87f141b0 /dev | |
| parent | ee711f8994d5e2e94cc61292ac6aab125c23df1c (diff) | |
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
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/db | 2 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 5 |
2 files changed, 5 insertions, 2 deletions
@@ -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 |