aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
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
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-02-20add changelog for 13867Enrico Tassi
2021-02-14Show "Error:"/"Warning:" with white type (on red/orange background)Jim Fehrle
2021-02-11Merge PR #13831: Properly document the local and global locality attributes.coqbot-app[bot]
Reviewed-by: gares Reviewed-by: jfehrle Ack-by: SkySkimmer
2021-02-09Merge PR #13822: Remove deprecated command line argumentscoqbot-app[bot]
Reviewed-by: gares
2021-02-09Merge PR #13810: ide: shift+enter to find backwardscoqbot-app[bot]
Reviewed-by: herbelin
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-29add changelogOlivier Laurent
2021-01-28Merge PR #13799: Replace : term with : type in open binders.coqbot-app[bot]
Reviewed-by: jfehrle
2021-01-28Merge PR #13789: Document limitation of rewrite regarding occurrence selection.coqbot-app[bot]
Reviewed-by: jfehrle Reviewed-by: silene
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]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
And update the doc_grammar files.
2021-01-28Apply suggestions from code reviewThéo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
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]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
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
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-25Update doc/sphinx/addendum/micromega.rstFrédéric Besson
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-22changelogBESSON Frederic
2021-01-22Merge PR #13754: Improve doc of occurrences and rewrite.coqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-22[micromega] Deprecate hopefully useless options and flagsBESSON Frederic
The goal is to eventually only use the Simplex solver and remove all the code needed for fourier elimination.
2021-01-22Improve doc of occurrences and rewrite.Jim Fehrle
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-01-22Add documentation for Ltac2 Printf.Pierre-Marie Pédrot
2021-01-22Add a type of format strings to Ltac2.Pierre-Marie Pédrot
It provides an abstract type of well-typed format strings, a scope to parse them and a minimal printf-like API.
2021-01-21Improve wording for #13384Jim Fehrle
2021-01-21Merge PR #13764: Remove Add InjTyp and 10 other micromega commands ↵BESSON Frederic
(deprecated in 8.13) Reviewed-by: Zimmi48 Reviewed-by: fajb
2021-01-20Remove double induction tacticJim Fehrle
2021-01-20Fix: "tactic" is not a tactic, so can't begin a .. tacn::Jim Fehrle
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵Pierre-Marie Pédrot
pattern Reviewed-by: ppedrot
2021-01-19Merge PR #13725: Support locality attributes for Hint Rewrite (including export)Pierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: gares Reviewed-by: ppedrot
2021-01-18Adding changelog for #13512.Hugo Herbelin
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` ↵Pierre-Marie Pédrot
into `pat:` Ack-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-01-18Add changelogPierre Roux
2021-01-18Merge PR #13705: Improve documentation of rewrite_strat/innermost and outermostcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: gares
2021-01-13Adjust the doc_grammar files.Théo Zimmermann
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:42:42 +0000