aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Collapse)Author
2020-11-20Merge PR #13265: Add support for general non-necessarily-recursive binders ↵coqbot-app[bot]
in notations Reviewed-by: ejgallego Ack-by: Zimmi48 Ack-by: jfehrle
2020-11-20Merge PR #13352: Configure default value of -native-compilercoqbot-app[bot]
Reviewed-by: erikmd Reviewed-by: silene Ack-by: mattam82 Ack-by: Blaisorblade Ack-by: gares Ack-by: Zimmi48 Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-20Add changelog for #13265.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-20Add changelogPierre Roux
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions ↵coqbot-app[bot]
between variable and non-qualified global references Reviewed-by: ejgallego Ack-by: maximedenes Ack-by: gares
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2020-11-20Update ↵Hugo Herbelin
doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a ↵coqbot-app[bot]
primitive projection was wrongly supposed to be already inferred Reviewed-by: gares
2020-11-19Adding changelog for #13237.Hugo Herbelin
2020-11-19[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.Théo Zimmermann
2020-11-19Add changelog for #13386.Hugo Herbelin
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ↵coqbot-app[bot]
then by last imported Reviewed-by: Zimmi48 Ack-by: RalfJung Ack-by: gares
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog.
2020-11-18Adding change log for #12765.Hugo Herbelin
2020-11-17Adding change log for #12984.Hugo Herbelin
Co-authored-by: Ralf Jung <post@ralfj.de>
2020-11-17Add changelog for #12986.Hugo Herbelin
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-16Merge PR #13040: [gc] Set GC policy as best-fit in OCaml >= 4.10.0coqbot-app[bot]
Reviewed-by: gares Reviewed-by: ppedrot
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Add change log for #12965.Hugo Herbelin
2020-11-16[gc] Set GC policy as best-fit in OCaml >= 4.10.0Emilio Jesus Gallego Arias
Closes #11277 ; the `space_overhead` parameter has been selected for maximum speedup, in some cases it could also increase memory consumption. Please use `OCAMLRUNPARAM` to tune it and report back your experiments.
2020-11-16Add changelog for #13337.Hugo Herbelin
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context ↵coqbot-app[bot]
of the definition of the metas Reviewed-by: mattam82
2020-11-16Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` ↵Pierre-Marie Pédrot
commands Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part ↵coqbot-app[bot]
of unification Reviewed-by: mattam82
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot
2020-11-16Merge PR #12685: Propagating scope information in indirect application to a ↵Pierre-Marie Pédrot
reference. Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-11-16Document the deprecation of the commands.Pierre-Marie Pédrot
2020-11-16Document the new warning.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
Reviewed-by: silene Reviewed-by: gares Reviewed-by: Zimmi48
2020-11-16Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freecoqbot-app[bot]
Reviewed-by: anton-trunov Reviewed-by: Blaisorblade
2020-11-16Changelog for variance syntaxGaëtan Gilbert
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ↵coqbot-app[bot]
sort elimination constraints Reviewed-by: gares
2020-11-16Slight improvement to the changelog entry.Théo Zimmermann
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
2020-11-15Add changelog for #13387.Hugo Herbelin
2020-11-15Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an ↵coqbot-app[bot]
error, not an anomaly Reviewed-by: ejgallego
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a ↵coqbot-app[bot]
handler in NotFoundInstance Reviewed-by: ejgallego
2020-11-15Document the new export locality for the remaining hint commands.Pierre-Marie Pédrot
2020-11-15Add changelog for #13383.Hugo Herbelin
2020-11-15Doc and changelog for Instance Generalized OutputGaëtan Gilbert
2020-11-15Adding change log for #12685.Hugo Herbelin
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not ↵Pierre-Marie Pédrot
a keyword. Ack-by: SkySkimmer Reviewed-by: herbelin Ack-by: ppedrot
2020-11-14Add changelog for #13376.Hugo Herbelin
2020-11-13Add changelog for #13373.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-08 12:03:52 +0000