aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-11[stm] Simplify logic involving forced futures.Emilio Jesus Gallego Arias
After the previous commit, we don't need to chain a dummy future anymore.
2020-06-11[declare] Remove some unused `fix_exn`Emilio Jesus Gallego Arias
In the current proof save path, the kernel can raise an exception when checking a proof wrapped into a future. However, in this case, the future itself will "fix" the produced exception, with the mandatory handler set at the future's creation time. Thus, there is no need for the declare layer to mess with exceptions anymore, if my logic is correct. Note that the `fix_exn` parameter to the `Declare` API was not used anymore. This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from pre-github times, so unfortunately I didn't have access to the discussion. We need to be careful in `perform_buildp` as to catch the `Qed` error and properly notify the STM about it with `State.exn_on`; this was previously done by the declare layer using a hack [grabbing internal state of the future, that the future itself was not using as it was already forced], but we now do it in the caller in a more principled way. This has been tested in the case that tactics succeed but Qed fails asynchronously.
2020-06-11Merge PR #12481: Minor improvements to the sections on basics and sorts.Emilio Jesus Gallego Arias
Reviewed-by: jfehrle
2020-06-11Merge PR #12492: Fix Windows addons.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 06:42:13 +0000