aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Collapse)Author
2019-10-05Changelog for SProp onGaëtan Gilbert
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive ↵Frédéric Besson
projections Reviewed-by: fajb
2019-10-03fix 10765-micromega-caches.rstFrédéric Besson
2019-10-03Improved handling of micromega cachesFrédéric Besson
- Specialised hash and equality functions. Avoid collisions in extreme scenarios. - Flags to disable the use of the caches. fixes #10772
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-24Merge PR #10774: Make `zify` does work for `Z.to_N`Frédéric Besson
Reviewed-by: Zimmi48 Reviewed-by: fajb
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
Reviewed-by: mattam82
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot Ack-by: vbgl
2019-09-17Add changelog entryMaxime Dénès
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
This helps extraction by not building sigT which can lower to Prop by template polymorphism. Bug #10757 can probably still be triggered by using module functors to hide that we're using Prop from Program Fixpoint but that's probably unfixable without fixing extraction vs template polymorphism in general. In passing we notice that Program doesn't know how to telescope SProp arguments, we would need a bunch of variants of sigma types to deal with it (or use Box?) so let's figure it out some other time. We also reuse the universe instance to avoid generating a bunch of short-lived universes in the universe polymorphic case.
2019-09-16Re-implementation of zifyFrédéric Besson
The logic is implemented in OCaml. By induction over the terms, guided by registered Coq terms in ZifyInst.v, it generates a rewriting lemma. The rewriting is only performed if there is some progress. If the rewriting fails (due to dependencies), a novel hypothesis is generated. This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848 ans fixes #10755. The zify plugin is placed in the micromega directory. (Though the reason is unclear, having it in a separate directory is bad for efficiency.) efficiency impact. There are also a few improvements of lia/lra that are piggybacked. - more aggressive pruning of useless hypotheses - slightly optimised conjunctive normal form - applies exfalso if conclusion is not in Prop - removal of Timeout in test-suite
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2019-09-05Merge PR #10731: Ocfnash/stdlib additionsHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2019-09-04Add changelog entry for 10731Oliver Nash
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-09-03Apply suggestions from code reviewOliver Nash
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-09-03New lemmas for List.vOliver Nash
* filter_app (moved from MSets/MSetRBT.v) * filter_map * filter_ext_in * ext_in_filter * filter_ext_in_iff * filter_ext * concat_filter_map * combine_nil * combine_firstn_l * combine_firstn_r * combine_firstn * nodup_fixed_point
2019-09-01edits per reviewYishuai Li
2019-09-01Changelog: more accurate on unconsYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
Fix changelog entry Fix build of the user manual Markup fixes from Théo Zimmermann Update doc and changelog and improve error messages.
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-09Add a changelog entryKazuhiko Sakaguchi
Acknowledgement: This work is financially supported by Peano System Inc. on-behalf-of: @peano-system <info@peano-system.jp>
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations ↵Maxime Dénès
involving & Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Ack-by: ggonthier Ack-by: herbelin Reviewed-by: maximedenes Ack-by: vbgl
2019-08-08[doc][ssr][under][setoid] Add changelog entryErik Martin-Dorel
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
Ack-by: Zimmi48 Ack-by: silene
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-29Document changes by PR 10324Vincent Laporte
White spaces are forbidden in the “&ident” syntax for ltac2 references.
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
The ExtrOCamlInt63 module can be required to map primitives from the Int63 module to their OCaml implementation (module Uint63 from the kernel).
2019-07-18Shorten changelogVincent Semeria
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. ↵Vincent Semeria
Redefine classical real numbers as a quotient of those constructive real numbers.
2019-07-11Merge PR #10439: Uniform handling of side-effects for opaque definitionsMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes
2019-07-08Adding a changelog.Pierre-Marie Pédrot
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
The changes are large due to `Pervasives` deprecation: - the `Pervasives` module has been deprecated in favor of `Stdlib`, we have opted for introducing a few wrapping functions in `Util` and just unqualified the rest of occurrences. We avoid the shims as in the previous attempt. - a bug regarding partial application have been fixed. - some formatting functions have been deprecated, but previous versions don't include a replacement, thus the warning has been disabled. We may want to clean up things a bit more, in particular w.r.t. modules once we can move to OCaml 4.07 as the minimum required version. Note that there is a clash between 4.08.0 modules `Option` and `Int` and Coq's ones. It is not clear if we should resolve that clash or not, see PR #10469 for more discussion. On the good side, OCaml 4.08.0 does provide a few interesting functionalities, including nice new warnings useful for devs.
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.Théo Zimmermann
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ↵Kazuhiko Sakaguchi
new one
2019-06-17Fix the changelog of 8.10+beta2 following the backport of #10205.Théo Zimmermann
2019-06-16Changelog for 8.10+beta2.Théo Zimmermann
2019-06-13Add missing changelog entry for #10360.Théo Zimmermann
2019-06-12Merge PR #10329: Update changelog for 10302 and 10305Théo Zimmermann
Reviewed-by: Zimmi48
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic ↵Théo Zimmermann
definitions Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ggonthier Reviewed-by: herbelin
2019-06-09Merge PR #10245: Command line: adding variants for Require, aligning on the ↵Emilio Jesus Gallego Arias
vernac syntax Reviewed-by: cpitclaudel Reviewed-by: ejgallego Ack-by: herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 17:02:54 +0000