aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-06-19Factorize hint flags in Class_tatcis.make_make_resolve_hyp.Pierre-Marie Pédrot
2020-06-18Merge PR #12536: tactics.rst: fix typo — readd `cbv` to title of its sectionThéo Zimmermann
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
2020-06-17Merge PR #12508: Fix #12507 Anomaly when using a ssreflect `reflect` viewCyril Cohen
2020-06-17Merge PR #12506: [toplevel] Annotate tailcall functionsEnrico Tassi
2020-06-16make the linter happyEnrico Tassi
2020-06-15Merge PR #12509: updated ci for unicoqThéo Zimmermann
2020-06-15updated ci for unicoqbeta
2020-06-15Merge PR #11906: [micromega] native support for boolean operatorsMaxime Dénès
2020-06-15[ssr] fix env handling in error message (fix #12507)Enrico Tassi
2020-06-15[ssr] remove catch allEnrico Tassi
2020-06-15Merge PR #12494: [dev/ci/nix] Support for building the Gappa plugin.Vincent Laporte
2020-06-14Update zify documentationFrédéric Besson
2020-06-14fix according to review by @pi8027Frédéric Besson
2020-06-14Update theories/micromega/ZifyBool.vFrédéric Besson
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-06-13[toplevel] Annotate tailcall functionsEmilio Jesus Gallego Arias
2020-06-12Merge PR #12357: [declare] Remove some unused `fix_exn`Enrico Tassi
2020-06-12Merge PR #12498: [dune] [dbg] Fix coqide target after CoqIDE move.Maxime Dénès
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
2020-06-11[declare] Remove some unused `fix_exn`Emilio Jesus Gallego Arias
2020-06-11Merge PR #12481: Minor improvements to the sections on basics and sorts.Emilio Jesus Gallego Arias
2020-06-11Merge PR #12492: Fix Windows addons.Emilio Jesus Gallego Arias
2020-06-11[dune] [dbg] Fix coqide target after CoqIDE move.Emilio Jesus Gallego Arias
2020-06-11Merge PR #12443: Fix #12442: Confusing error message when the intro pattern o...Pierre-Marie Pédrot
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
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
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
2020-06-09Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n t...Vincent Semeria
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
2020-06-09Summary of changes for 8.12Matthieu Sozeau
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
2020-06-08Add NOTINRSTS nonterminal to suppress messagesJim Fehrle
2020-06-08Report an error for empty (sub)productionsJim Fehrle
2020-06-08Add MOVEALLBUT operationJim Fehrle