aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2020-11-16Tentative fix for the refman.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
2020-11-16Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freecoqbot-app[bot]
2020-11-16Update grammar in docJim Fehrle
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]
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-15Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block verbati...Li-yao Xia
2020-11-15Add changelog for #13387.Hugo Herbelin
2020-11-15Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error...coqbot-app[bot]
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...coqbot-app[bot]
2020-11-15Merge PR #13368: Fix dune rules for @check-gram following recent changes.coqbot-app[bot]
2020-11-15Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve d...coqbot-app[bot]
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 a...Pierre-Marie Pédrot
2020-11-15Merge PR #13356: Make the universe of primitive arrays irrelevantPierre-Marie Pédrot
2020-11-14Documenting one-line verbatim.Hugo Herbelin
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-14Add changelog for #13376.Hugo Herbelin
2020-11-13Add changelog for #13373.Hugo Herbelin
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-13Fix dune rules for @check-gram following recent changes.Théo Zimmermann
2020-11-13Merge PR #12420: [stdlib] Decidable instance for negationcoqbot-app[bot]
2020-11-13Add changelog for #13365Li-yao Xia
2020-11-12Add changelog entry for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Move last changelog entry for 8.12.1.Théo Zimmermann
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...coqbot-app[bot]
2020-11-12Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.coqbot-app[bot]
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-12Add changelog for #13345.Hugo Herbelin
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
2020-11-11We move the example of Makefile wrapper next to the explanations about CoqMak...Hugo Herbelin
2020-11-11Add changelog for #13351.Hugo Herbelin
2020-11-10Merge PR #13315: Convert logic chapter to prodncoqbot-app[bot]
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-10Merge PR #13325: [compat] remove 8.10coqbot-app[bot]
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-09Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml...coqbot-app[bot]
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-09Remove virtually unused replace rule.Théo Zimmermann
2020-11-09Fix #5226: Add index entry for ::=.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:24:58 +0000