aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-15[micromega] Use `minus_one` built-in zarith constant.Emilio Jesus Gallego Arias
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-15Updated .csdp.cache.test-suite and minor fixesBESSON Frederic
- merlin.in : added zarith - test-suite/Makefile remove .csdp.cache on make clean updated .csdp.cache.test-suite
2020-09-15[micromega] [test-suite] Update csdp cache for num -> zarith migrationEmilio Jesus Gallego Arias
2020-09-15[micromega] Migrate from num to zarithEmilio Jesus Gallego Arias
We still link num in `coqc` , that will be removed in a separate step. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-09-15[micromega] call csdpcert using path.Emilio Jesus Gallego Arias
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: pi8027 Reviewed-by: ppedrot
2020-09-15Merge PR #12972: [ci] [docker] Up testing to OCaml 4.11.1coqbot-app[bot]
Reviewed-by: Zimmi48
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-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-09-14[nix] Update ref for ocamlformat 0.15Emilio Jesus Gallego Arias
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-14[ocamlformat] Update to ocamlformat 0.15.0Emilio Jesus Gallego Arias
This is necessary to support OCaml 4.11 in development.
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
- `odoc` must be bumped to support 4.11
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-13Add overlays.Pierre-Marie Pédrot
2020-09-13Statically ensure that only polymophic hint terms come with a context.Pierre-Marie Pédrot
It is the duty of the caller to properly declare monomorphic global constraints when creating a non-globref hint. All callers were already abiding by this convention.
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-11Propagate zarith dependency.Théo Zimmermann
External plugins need the OCaml dependencies of Coq in scope because ocamlfind looks for them since #12604.
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-10Use fresher names in eqschemes.Jasper Hugunin
The previous implementation appears to be sound when Mangle Names is off, but it relies on two fragile assumptions, namely that next_global_ident_away always returns different identifiers when called with naming hints which are different after stripping all digits from the end, and that default_id_of_sort (locally defined) never returns "HC" or "P", or either of those followed by a string of digits. These changes make both assumptions unnecessary. As a side note, it seems odd that fresh is ignoring it's env parameter.
2020-09-10Fix typos.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-09-10When a notation is only parsing, do not attach to it a specific format.Hugo Herbelin
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-09dune: pass -bin-annot to configureGaëtan Gilbert
This ends up in coq_makefile's CAMLFLAGS so we need it to make merlin work properly.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 01:43:13 +0000