99901e969c
Changes from V8.3 to V8.3pl1 o Type inference, notations and implicit arguments bug fixes - #2448 (alpha-renaming problems with notations internally using binders) - #2454 (pattern-matching sometimes not supporting type casts) - fixing combined use of non-implicit and explictly-declared implicit arguments in inductive arities - restored support for using some ident with different scopes in notations o Ltac and tactics bug fixes - #2414 (rewrite in not looking for eq_ind in the right module) - #2433 (new "is_evar"/"has_evar" to restore support for matching evars in Ltac) - #2453 (dependent destruction) - loop in dependent destruction - new "constr_eq" tactic for restoring support for term equality test in Ltac - setoid rewrite under cases and abstraction fixed o Coqdoc and documentation bugs - #2418 (wrong URLs in documentation) - #2441 (coqdoc bug in Mergesort.v) - #2445 (correct support for "'" character in coqdoc links to notations) - fixed wrong use of "moduleid" instead of "module" in coqdoc html indexes - fixing parsing of Multiplication and Division signs (unicode 0xD7 and 0xF7) o Compilation - #2432 (support for compilation with camlp5 6.02.0) - support for compilation with ocaml >= 3.09.3 restored o Extraction - #2413 (prevent type-unsafe optimisations of pattern matching) - Identifiers of a development aimed to be extracted should avoid containing "__", since the extraction make various use of this sub-string, leading to potential name clashes. This was already so in V8.3, but not announced, as mentionned by #2421. o Miscellaneous bug fixes - #2412 (anomaly Ploc.Exc when using Ltac Debug) - #2419 (redundant opp_compare removed) - #2427 (Module Functor claims Signature does not match) - #2431 (compliance of CoqIDE use of mutexes with FreeBSD) - #2434 (anomaly DuringSyntaxChecking with Local/Global prefixes) - a few improvements in efficiency |
||
|---|---|---|
| .. | ||
| patch-ac | ||