aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-06Merge PR #13586: Support nested timeoutsPierre-Marie Pédrot
2021-03-06Merge PR #13882: Fix #12011 ssreflect "rewrite in" with setoidsPierre-Marie Pédrot
2021-03-06Merge PR #13236: Add a type of format strings to Ltac2.Michael Soegtrop
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
2021-03-04Correctly sort the glossaryJim Fehrle
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
2021-03-04Properly support nested timeoutsLasse Blaauwbroek
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
2021-03-03Merge PR #12567: [build] Split stdlib to it's own package.coqbot-app[bot]
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ...coqbot-app[bot]
2021-03-02Dead code elimination: not reducible error message is never raised.Théo Zimmermann
2021-02-28Merge PR #13853: Delay the dynamic linking of native-code libraries until nat...Pierre-Marie Pédrot
2021-02-28Fix link of default_bindings.slb Prime
2021-02-27Merge PR #13876: [coqc] Don't allow to pass more than one file to coqccoqbot-app[bot]
2021-02-27Add changelogPierre Roux
2021-02-27Remove decimal-only number notationsPierre Roux
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
2021-02-26Signed primitive integersAna
2021-02-26Delay the dynamic linking of native-code libraries until native_compute is ca...Guillaume Melquiond
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-22mention --version to CoqIDEEnrico Tassi
2021-02-22changelog for 8.13.1Enrico Tassi
2021-02-20Update doc/changelog/01-kernel/13867-changelog-for-13867.rstEnrico Tassi
2021-02-20add changelog for 13867Enrico Tassi
2021-02-11Merge PR #13831: Properly document the local and global locality attributes.coqbot-app[bot]
2021-02-09Merge PR #13822: Remove deprecated command line argumentscoqbot-app[bot]
2021-02-09Merge PR #13810: ide: shift+enter to find backwardscoqbot-app[bot]
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-02-05Fix hierarchy of sections in module chapter.Théo Zimmermann
2021-02-04Changelog for #13822Gaëtan Gilbert
2021-02-01Add changelog entryslrnsc
2021-01-28Merge PR #13799: Replace : term with : type in open binders.coqbot-app[bot]
2021-01-28Merge PR #13789: Document limitation of rewrite regarding occurrence selection.coqbot-app[bot]
2021-01-28Update doc/sphinx/proofs/writing-proofs/rewriting.rstJim Fehrle
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
2021-01-28Apply suggestions from code reviewThéo Zimmermann
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
2021-01-28Document how rewrite works regarding occurrence selection.Théo Zimmermann
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-25Update doc/changelog/04-tactics/13781-deprecate_micromega_options.rstFrédéric Besson
2021-01-25Update doc/sphinx/addendum/micromega.rstFrédéric Besson
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:44:19 +0000