aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-15[ssr] remove catch allEnrico Tassi
2020-06-15Merge PR #12494: [dev/ci/nix] Support for building the Gappa plugin.Vincent Laporte
Reviewed-by: vbgl
2020-06-14Update zify documentationFrédéric Besson
Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14fix according to review by @pi8027Frédéric Besson
2020-06-14Update theories/micromega/ZifyBool.vFrédéric Besson
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> - insert boolean constraint (b = true \/ b = false) - add specs for b2z - zify_post_hook performs a case-analysis over boolean constraints - Stricter typing constraints for `zify` declared operators The type is syntactically checked against the declaration of injections. Some explicit casts may need to be inserted.
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-06-13[toplevel] Annotate tailcall functionsEmilio Jesus Gallego Arias
This will ensure that we don't introduce problems as it has happened in the past. While we are at it, we fix one easy case of non-tail call.
2020-06-12Merge PR #12357: [declare] Remove some unused `fix_exn`Enrico Tassi
Reviewed-by: gares
2020-06-12Merge PR #12498: [dune] [dbg] Fix coqide target after CoqIDE move.Maxime Dénès
Reviewed-by: maximedenes
2020-06-11[test-suite] [stm] Interactive test case for fail-on-qed.Emilio Jesus Gallego Arias
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-11[dune] [dbg] Fix coqide target after CoqIDE move.Emilio Jesus Gallego Arias
Fixes #12496
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 13:56:06 +0000