aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-14Correct dependencies in the micromega packChantal Keller
2019-03-13Merge PR #9736: Don't coqchk the test suite prerequisitesEnrico Tassi
Reviewed-by: gares
2019-03-13Merge PR #9757: [refman] Add 'warn' option to coqtop directive.Emilio Jesus Gallego Arias
Reviewed-by: cpitclaudel
2019-03-13Merge PR #9723: Fix undefined gramlib_MLLIB_DEPENDENCIES in make installEnrico Tassi
Reviewed-by: gares
2019-03-13Merge PR #9739: [dune] [configure] Fix `gramlib` path for hardcoded includes.Enrico Tassi
Reviewed-by: gares
2019-03-13Merge PR #9748: [dune] Add shim for coqtop.byteThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-03-13[refman] Fix Sphinx-translation regression in Arguments command.Théo Zimmermann
2019-03-13[refman] Remove warning silencing by fixing the underlying issue.Théo Zimmermann
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-03-13Merge PR #9627: Small retroknowledge/primitive cleanupVincent Laporte
Ack-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: vbgl
2019-03-12[refman] Add 'warn' option to coqtop directive.Théo Zimmermann
Fix semantic conflict between #9389 and #9654.
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: ppedrot
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ↵Emilio Jesus Gallego Arias
record Reviewed-by: ejgallego
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
Ack-by: gares Ack-by: herbelin Ack-by: mattam82 Ack-by: ppedrot
2019-03-12[dune] Add shim for coqtop.byteEmilio Jesus Gallego Arias
We add a shim for running the byte version of coqtop. This fixes the Coq part of #9727 , the Dune part is still open at https://github.com/ocaml/dune/issues/108 but this PR includes a workaround. Unfortunately we have to introduce a small inefficiency in the build process as we build both byte and native versions of plugins for this work reliable. As this is a choice done during bootstrap it won't be easy to fix until we have our own `dune coqtop` command and we can control the rules depending on the final target. This should affect the `check` target so still fast builds should be possible, but if this is a problem we could add a `byteboot` target to help.
2019-03-12Merge PR #9738: [ci] [docker] Upgrade odoc to 1.4.0Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-03-11[dune] [configure] Fix `gramlib` path for hardcoded includes.Emilio Jesus Gallego Arias
The regular make build uses a non-standard header path for their files [as a way to workaround the ugliness of the non-hygienic build] This breaks in Dune as it uses the regular object file pack, so `coq_makefile` won't find it. We cherry pick a change from #8729 which fixes the updated version of bug #9735 , even tho `coq_makefile` should stop relying on hardcoded paths and use findlib instead. Closes #9735
2019-03-11[ci] [docker] Upgrade odoc to 1.4.0Emilio Jesus Gallego Arias
This is routine as for API doc writers to be able to access the newer features.
2019-03-11Don't coqchk the test suite prerequisitesGaëtan Gilbert
This causes the makefile to break due to dependencies when it fails, and it's not worth adding a whole mess of code to catch the failure for these files.
2019-03-11Fix undefined gramlib_MLLIB_DEPENDENCIES in make installGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
This operation is done directly in Safe_typing.register_inline and has nothing to do with retroknowledge afaict.
2019-03-11Merge PR #9698: Remove last random failuresGaëtan Gilbert
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego
2019-03-11Merge PR #9675: Dune: remove -short-paths flag.Emilio Jesus Gallego Arias
Ack-by: ejgallego Reviewed-by: gares
2019-03-11Merge PR #9570: Refresh contributing guide and README.Maxime Dénès
Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2019-03-10Merge PR #9654: [sphinx] Add warn option to coqtop directive.Clément Pit-Claudel
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: vbgl Reviewed-by: cpitclaudel
2019-03-10Merge PR #9728: Fix issue #9722 pkg-config not foundThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-08Fix issue #9722 pkg-config not foundMichael Soegtrop
2019-03-08Merge PR #9720: [refman] Fix typo in local application of tacticsThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-08[sphinx] Fix typo in local application of tacticshawnzug
2019-03-07Merge PR #9133: Move README-V1-V5 to credits chapterClément Pit-Claudel
Reviewed-by: cpitclaudel
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-03-05Merge PR #9524: Fix #7632: Change syntax of autoapply according to the ↵Pierre-Marie Pédrot
documentation. Reviewed-by: ppedrot
2019-03-05Merge PR #9701: [CI] Add stdlib2Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-05[CI] Add stdlib2Vincent Laporte
2019-03-05Remove regularly failing test from test-suite.Théo Zimmermann
2019-03-05Put regularly failing async tests in allow_failure mode.Théo Zimmermann
2019-03-04Merge PR #9687: Cleanup exported variables in Makefile.buildEnrico Tassi
Reviewed-by: gares
2019-03-04Merge PR #8700: Removing debugging warning when no exception handler is ↵Emilio Jesus Gallego Arias
registered in futures Ack-by: ejgallego
2019-03-04Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-04Removing debugging warning when no exception handler is registered in futures.Hugo Herbelin
As far as I understood, this was useful for tine-tuning the stm but this is no longuer needed: it is ok not to have exception handler when a constant registration does not span over several commands (such as "Goal ... Qed" or obligations).
2019-03-04Merge PR #9660: Set COQLIB so the test suite runs locally on Windows.Enrico Tassi
Reviewed-by: ejgallego Ack-by: SkySkimmer Ack-by: gares Ack-by: jfehrle Ack-by: vbgl
2019-03-04[stm] unfocus when edition exits the proof (fix #9431)Enrico Tassi
2019-03-04Merge PR #9594: When Nix build is finished and pushed to Cachix, update a ↵Maxime Dénès
specific branch. Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: maximedenes Reviewed-by: vbgl
2019-03-04Merge PR #9047: [dune] Shim for starting `coqtop/coqide` with minimal config.Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: rgrinberg
2019-03-03Cleanup exported variables in Makefile.buildGaëtan Gilbert
2019-03-03[dune] Shim for starting `coqtop/coqide` with minimal config.Emilio Jesus Gallego Arias
As requested by Gaëtan Gilbert, we add shims - `dev/shim/coqtop-prelude` - `dev/shim/coqide-prelude` that will build and start `coqtop` and `coqide` with just the prelude loaded properly. `dune exec dev/shim/coqtop-prelude` will build and execute this shim, equivalent to doing `make states && bin/coqtop` under the old model. This PR is just a bit of "a hack" until proper support for Coq libraries arrives to Dune, however there is nothing wrong with it. In particular, we must bootstrap `coq.plugins.ltac` as Dune needs to compute the full installation path to allow `%{bin:foo}` in deps, [this is a kind of shortcoming of the current implementation, and the error message is just terrible] We cannot depend on installed `.vo` files without doing a gross hack [including them inside an ml lib] so for now we just depend on their non-installed forms. Using `%{bin}` is good enough for the shims who would like to locate binaries using `PATH`. The long term plan (for now) is to have a command similar to `dune utop $dir`, `dune coqtop $dir`, which would spawn a proper Coq shell with the corresponding libraries on the path. This will work for `dir=stdlib/Init/` for example, or for any other combination.
2019-03-01Merge PR #9676: Move test_mode from Flags to Vernacentries (use point)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-01Merge PR #9624: [Kernel] Simpler generation of opcode filesEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: rgrinberg Ack-by: vbgl
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 03:22:46 +0000