aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-14[CI] Always upload artifactsJason Gross
In order to support the workflow where coqbot automatically turns failing CI jobs into minimized examples for the test-suite easily (https://github.com/coq/bot/issues/107), we want to be able to get all of the .v files and all of the generated .vo and .glob files in the artifact, even when the build fails.
2020-09-14Merge PR #13014: [ci] [mathcomp] run the test suitecoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-14Merge PR #13022: Fixing documentation relatively to example of use of extra ↵coqbot-app[bot]
spaces in notations Reviewed-by: jfehrle
2020-09-13Fixing documentation relatively to example of use of extra spaces in notations.Hugo Herbelin
2020-09-12Merge PR #12979: Uniformize names for number literals between parsing and refmancoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: Zimmi48 Ack-by: proux01
2020-09-11[numeral notation] Improve documentationPierre Roux
Following reviews from Jim Fehrle on #12218 and #12979
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11Turn integer into natural in several mlgsPierre Roux
Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
2020-09-11[refman] Explicit integer and naturalPierre Roux
As respectively bigint and bignat that fit into an OCaml int.
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename numeral to numberPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-11[parsing] Simplify bigintPierre Roux
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-09-11[refman] Replace num by intPierre Roux
num stands for natural numbers whereas the text deals with negative values.
2020-09-11Merge PR #13011: Minimal changes to make the refman compatible with Sphinx 3.coqbot-app[bot]
Reviewed-by: cpitclaudel Reviewed-by: jfehrle Ack-by: Zimmi48
2020-09-11[ci] [mathcomp] run the test suiteEnrico Tassi
2020-09-11Remove outdated references to productionlist.Théo Zimmermann
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-09-11Merge PR #13005: Add simple-io to dev/ci/nix.Vincent Laporte
Reviewed-by: vbgl
2020-09-10Merge PR #13001: Update INSTALL.mdcoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-09-10Fix typos.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-09-10Add simple-io to dev/ci/nix.Théo Zimmermann
2020-09-10Merge PR #12997: Add a fast-path to Tactics.e_change_in_hyps.Hugo Herbelin
Reviewed-by: herbelin
2020-09-10Merge PR #12998: changelog entry for 12857coqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-10Add a fast-path to Tactics.e_change_in_hyps.Pierre-Marie Pédrot
In case we give an empty list of occurrences to e_change_in_hyps, we can return immediately. This saves the allocation of a dummy evar, and a O(n) map over the context for "local" reduction functions. Note that passing an empty list of hypotheses is the default for both the "change" tactic and reduction tactics.
2020-09-10Update doc/changelog/06-ssreflect/12857-changelog-for-12857.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-09Update INSTALL.mdMatthieu Sozeau
2020-09-09Merge PR #12994: Fix docgram's dune file following #12085.coqbot-app[bot]
Reviewed-by: ejgallego
2020-09-09Merge PR #12094: Extend app_inj_tail and other list lemmasHugo Herbelin
Reviewed-by: anton-trunov Ack-by: herbelin
2020-09-09changelog entry for 12857Enrico Tassi
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable ↵Pierre-Marie Pédrot
from initial evars Ack-by: JasonGross Ack-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: jfehrle Ack-by: maximedenes Reviewed-by: ppedrot
2020-09-09Merge PR #12905: Lint stdlib with -mangle-names #2coqbot-app[bot]
Reviewed-by: anton-trunov Ack-by: jashug Ack-by: olaure01
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: ppedrot
2020-09-08Fix docgram's dune file following #12085.Théo Zimmermann
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type ↵coqbot-app[bot]
in collections Reviewed-by: gares Ack-by: Zimmi48
2020-09-08Merge PR #12991: [Small typo] Update match.rstcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-08[Small typo] Update match.rstClément Blaudeau
Some error messages were merged together
2020-09-08Merge PR #12927: Explain that tactics applied to multiple goals don't ↵coqbot-app[bot]
preserve the order Reviewed-by: Zimmi48 Ack-by: chdoc Ack-by: jfehrle
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see ↵Pierre-Marie Pédrot
comment in #12944). Ack-by: RalfJung Ack-by: jashug Reviewed-by: ppedrot
2020-09-08Merge PR #12987: Fix printing of `change` tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-07Circumvent revealed bug of evar resolution for fixpointMaxime Dénès
This is to be removed once #12920 is merged.
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
The test is refined to handle aliases: i.e. undefined evars coming from restrictions and evar-evar unifications with an initial evar are not considered fresh unresolved evars. To check this, we generalize the restricted_evars set to an aliased_evars set in the evar map, registering evars being solved by another evar due to restriction or evar-evar unifications. This implements the proposal of PR #370 for testing the resolution status of evars independently of the evar-evar orientation order. This allows [apply] to refine an evar with a new one if it results from a [clear] request or an evar-evar solution only, otherwise the new evar is considered fresh and an error is raised. Also fixes bugs #4095 and #4413. Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
2020-09-07Merge PR #12988: Remove dead code in clenv-generating functions.Hugo Herbelin
Reviewed-by: herbelin
2020-09-07Explain how selectors change the order of goalsJim Fehrle
2020-09-07Remove dead code in clenv-generating functions.Pierre-Marie Pédrot
The *_env functions used to be different, but now they were just redundant with their direct equivalent.
2020-09-07Add changelog entryEdward Wang
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:23:29 +0000