aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-11Merge PR #12443: Fix #12442: Confusing error message when the intro pattern ↵Pierre-Marie Pédrot
of "apply in" fails Reviewed-by: ppedrot
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-10[dev/ci/nix] Support for building the Gappa plugin.Théo Zimmermann
2020-06-10Fix the build of Elpi by calling Dune directly.Théo Zimmermann
2020-06-10Merge PR #12491: Update changelog for 8.12+beta1.Clément Pit-Claudel
2020-06-10Call autoreconf in interval, flocq and gappa-plugin.Théo Zimmermann
2020-06-10Fix Coquelicot build in Windows add-ons.Théo Zimmermann
Adapted from 747936a9d9a7402f537e1e1a857c7591d8e88d2a
2020-06-10Windows: fix build of Gappa C++ toolMichael Soegtrop
2020-06-10Windows: fix menhir and coq-menhirlib build for latest version.Michael Soegtrop
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
Ack-by: Zimmi48 Reviewed-by: erikmd Reviewed-by: silene
2020-06-09Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n ↵Vincent Semeria
to 1/2^n Reviewed-by: VincentSe
2020-06-09Update dev/doc/critical-bugsPierre Roux
2020-06-09Merge sections on functions and function types.Théo Zimmermann
2020-06-09Minor improvements to the section on sorts.Théo Zimmermann
2020-06-09Minor improvements to the section on basics.Théo Zimmermann
2020-06-09Merge PR #12103: Convert Ltac chapter to prodnThéo Zimmermann
2020-06-09Merge PR #12462: Summary of changes for 8.12Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: gares Ack-by: jfehrle
2020-06-09Summary of changes for 8.12Matthieu Sozeau
Includes fixes to changes by Jim, Enrico and Théo Fix local links, for 8.12 and 8.11
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
- by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except - don't generate a name for cmdv and tacv - generate more flexibily for exn, warn and attr
2020-06-08Add NOTINRSTS nonterminal to suppress messagesJim Fehrle
2020-06-08Report an error for empty (sub)productionsJim Fehrle
(Sphinx notations don't support these.)
2020-06-08Add MOVEALLBUT operationJim Fehrle
2020-06-08Refactor SELF code for clarityJim Fehrle
Handle SELF within nested constructs more clearly
2020-06-08Fix 12483Pierre Roux
2020-06-08Merge PR #12482: [ci] [overlays] Pin unicoq to a stable version.Théo Zimmermann
Reviewed-by: Zimmi48
2020-06-08[ci] [overlays] Pin unicoq to a stable version.Emilio Jesus Gallego Arias
Following upstream advice.
2020-06-08Merge PR #12480: Don't suggest Proof using when no section variablesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-08Merge PR #12471: Fix uncaught NotArity in inductive typePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-06-08Merge PR #12477: [sphinx] Fix regexp used in ↵Théo Zimmermann
coqdomain.CoqtopBlocksTransform.split_lines Reviewed-by: Zimmi48
2020-06-08Merge PR #12451: Fix Flocq build on Windows.Emilio Jesus Gallego Arias
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
Fix #12447
2020-06-07[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_linesClément Pit-Claudel
2020-06-07Merge PR #12473: Match only a single line as the coqtop prompt in coqtop:: ↵Clément Pit-Claudel
directive
2020-06-06Match only a single line as the coqtop promptJim Fehrle
(the previous expression was including some expected output)
2020-06-06Merge PR #12380: Fix #12361 (indexing issues in the PDF)Théo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
Fixes #12390
2020-06-06Fix #12442: Confusing error message when the intro pattern of "apply in" failsAttila Gáspár
2020-06-05Fix Flocq build in Windows add-ons.Théo Zimmermann
1. Fix casing of build_prep_overlay argument. Follow-up of 6cc6b87f997d7a5e848203b49bfedfaa96c53bb2 2. Call autoconf directly. Adapted from a9996619e2d2352e0e60faf4dbde78fa1549b2af
2020-06-05Merge PR #12336: Factorize code in hint declaration.Hugo Herbelin
Reviewed-by: herbelin
2020-06-05Merge PR #12450: Document known issue of Proof <term> with PG.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: erikmd Reviewed-by: jfehrle
2020-06-05Merge PR #12460: Add remaining 8.12+beta1 changelog entries.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-05Merge PR #12459: Document incompatibility with Sphinx 3.Emilio Jesus Gallego Arias
Reviewed-by: cpitclaudel
2020-06-05Merge PR #12437: Fix ONLY_WINDOWS in .gitlab-ci.yml.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-05Merge PR #12397: Fix #12280: do not use xindy to avoid build failures on ↵Emilio Jesus Gallego Arias
some machines. Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2020-06-05Merge PR #12456: Fix version switcher when building with Dune.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-05Adjust list of versions in version switcher.Théo Zimmermann
- Use the name 'dev' instead of 'master' because it is less cryptic. - Add the 'v8.12' branch. - Use the branch version only for active branches, and the latest patch-level release for the rest.
2020-06-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 16:04:27 +0000