aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-03-24Merge PR #11703: Making of NumTok an API for numeralPierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: proux01
2020-03-23[ci] add metacoqMatthieu Sozeau
2020-03-22Overlay for QuickChickHugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-03-19[ocamformat] Update to 0.13.0Emilio Jesus Gallego Arias
We include the `version=0.13.0` field that should help users not to use the wrong version. `disable=true` still seems a noop with `dune`. There are some minor changes in the way comments are formatted; I'm unsure if this is due to the `wrap-comments` option; as always; tweaks to the config are most welcome.
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
There is a lot of check overhead in the code, we will try to provide a more convenient API for manipulation of remaining obligations.
2020-03-19[ci] Overlays for declare interface refactoring.Emilio Jesus Gallego Arias
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-19Merge PR #11860: [ci] [docker] Update to 4.09.1Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
Ack-by: herbelin
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-03-18[ci] [docker] Update to 4.09.1Emilio Jesus Gallego Arias
That release includes non trivial changes related C compilers, in particular due to `-fno-common` support.
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Adding overlays.Pierre-Marie Pédrot
2020-03-18Also show unchanged headers.Théo Zimmermann
2020-03-18Remove dates in headers.Théo Zimmermann
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
2020-03-16[ci] Cleanup old overlays.Emilio Jesus Gallego Arias
2020-03-16[ci] [docker] Update components in Docker imageEmilio Jesus Gallego Arias
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
2020-03-13Update Azure MacOS version 10.13 -> 10.14Gaëtan Gilbert
10.13 is deprecated as an azure VM Close #11449
2020-03-13Merge PR #11804: [CI] test hierarchy builder as part of elpiGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2020-03-12[ci] [doc] Point to actual docker instructions.Emilio Jesus Gallego Arias
2020-03-12Print implicit arguments in types of referencesSimonBoulier
2020-03-11Update dev/ci/ci-basic-overlay.shEnrico Tassi
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-11[CI] test hierarchy builder as part of elpiEnrico Tassi
2020-03-10Merge PR #11732: Update the OCaml version in `default.nix` to 4.09.0Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-10Merge PR #11764: Simplify mutual template polymorphismGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-09Do not erase OCAMLPATH in CI targets with Dune-built CoqMaxime Dénès
2020-03-09Add CI overlays.Pierre-Marie Pédrot
2020-03-06Merge PR #11717: [dune] [ocamldebug] Improve ocamldebug rulesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-04Add overlay for equations.Hugo Herbelin
2020-03-03Update the OCaml version in `default.nix` to 4.09.0Maxime Dénès
It is more convenient to use recent versions of OCaml while developing (better backtraces, etc).
2020-03-02Merge PR #11728: [dune] [doc] Be more explicit about coqtop dependenciesThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-01[ci] [docker] overlay for elpi 1.10Enrico Tassi
2020-03-01[ci] [docker] bump elpi to 1.10.2Enrico Tassi
2020-03-01[ci] bump dune to 2.0.1 due to upstream problemsEnrico Tassi
2020-03-01[dune] [doc] Be more explicit coqtop dependenciesEmilio Jesus Gallego Arias
Fixes #11726
2020-02-29[dune] [ocamldebug] Improve ocamldebug rulesEmilio Jesus Gallego Arias
We provide the closure of the dependencies manually. This is still a hack, but not so bad given that the `source`'d files still do contain that duplication too. Dune should provide this functionality so we can replace both this rule and the source files. Actually, that's not hard to implement, `utop` already supports a printer attribute so these are loaded automatically, so the ocamldebug mode could do the same. Should fix #11716
2020-02-25Merge PR #11669: Remove hard to read blue color in merge-prEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-25Merge PR #11674: [ci] Fix Coquelicot buildGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-24[ci] Fix Coquelicot buildEmilio Jesus Gallego Arias
New versions did remove the autogen.sh script in favor of plain `autoreconf` Note that the Coquelicot build documentation seems incorrect.
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
Raising inside exception printers is quite tricky as the order of registration for printers will indeed depend on the linking order. We thus forbid this, and make our API closer to the upstream `Printexn` by having printers return an option type.
2020-02-24Remove hard to read blue color in merge-prGaëtan Gilbert
2020-02-22Merge PR #11651: [merge-script] Improve warning in case of batch merging.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-22Merge PR #11638: Add debugger printer for type GlobEnv.tEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
Also renamed it to relative_entry_level. Correspondence between old and new representation is: (n,L) -> LevelLt n (n,E), (n,Prec n) -> LevelLe n (n,Any) -> LevelSome (n,Prec p) when n<>p was unused Should not change global semantics (except error message in pr_arg).
2020-02-21[merge-script] Improve warning in case of batch merging.Théo Zimmermann
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding ↵Emilio Jesus Gallego Arias
notation format + new notion of format associated to a given interpretation Ack-by: maximedenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:19:05 +0000