aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-04[stm] unfocus when edition exits the proof (fix #9431)Enrico Tassi
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-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
2019-03-01Merge PR #9677: Update coqdev.el to use -topfileEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-01Merge PR #9626: [lib] Add `Map.update` from OCaml 4.06Pierre-Marie Pédrot
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2019-03-01[Kernel] Simpler generation of opcode filesVincent Laporte
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program rather than a pipeline of sed and awk text processing.
2019-03-01write_uint63.ml: add headerVincent Laporte
2019-03-01Merge PR #9006: [dune] Add quickide target for building of IDE.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-03-01Update coqdev.el to use -topfileGaëtan Gilbert
PG would do it by default but since we override coq-prog-args it doesn't.
2019-03-01Move test_mode from Flags to Vernacentries (use point)Gaëtan Gilbert
2019-03-01[dune] Add quickide target for building of IDE.Emilio Jesus Gallego Arias
Note that `states` doesn't work reliably yet, but that is a separate problem that will be fixed in Dune 1.6. [Or we could also fix it improving the rules in envars.ml]
2019-03-01Merge PR #9656: Fix deprecation warningEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-01Merge PR #9610: Fix #9110: mention check-owners-pr.shEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: vbgl
2019-03-01Merge PR #9619: Print location for type error in pattern variableEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-01Merge PR #9672: [doc] ssr: Fix the documentation of `by [tacs]`Théo Zimmermann
Reviewed-by: gares
2019-03-01[doc] ssr: Fix the documentation of `by [tacs]`Erik Martin-Dorel
Closes coq/coq#9669
2019-02-28Fix #9110: mention check-owners-pr.shThéo Zimmermann
2019-02-28Merge PR #9621: [ide] only use Coq_config for the URL of the manualPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-02-28Print location for type error in pattern variableGaëtan Gilbert
See #9616
2019-02-28Merge PR #9578: Document primitive integersThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-02-28Merge PR #9649: [dune] Simple rule to generate Stdlib's documentation.Théo Zimmermann
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: rgrinberg
2019-02-27[ide] only use Coq_config for the URL of the manualEnrico Tassi
2019-02-27Merge PR #9622: Fix makefile deps for coqidePierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-02-27[make] coqide target needs STM workersEnrico Tassi
2019-02-27[ide] coqtop -> coqidetop in user messagesEnrico Tassi
2019-02-26[dune] Simple rule to generate Stdlib's documentation.Emilio Jesus Gallego Arias
Ideally this will be handled by Dune's native library support, but this could be useful for the likes of #9648. I am not sure what should be done w.r.t. style files.
2019-02-26Merge PR #9612: Fix #9526: Registering inductives for primitive integers ↵Vincent Laporte
doesn't check enough Ack-by: SkySkimmer Reviewed-by: vbgl
2019-02-26Fix deprecation warningEnrico Tassi
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-26Merge PR #9648: [Gitlab-CI] Deploy api documentation to GH-PagesEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: vbgl
2019-02-26Merge PR #9653: Fix gitattributes for Makefile.duneEmilio Jesus Gallego Arias
2019-02-26Fix gitattributes for Makefile.duneGaëtan Gilbert
Since it matches *.dune and Makefile* the later needs to come second in the gitattributes file.
2019-02-26Merge PR #9567: [vernac] Unify declaration hooks.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-02-25[Manual] Refactor documentation of internal registration commandsVincent Laporte
2019-02-25[Manual] Document primitive integersVincent Laporte
2019-02-25[Manual] Document the “Primitive” commandVincent Laporte
2019-02-25[Manual] Document “Register Inline”Vincent Laporte
2019-02-25[Manual] Document “Register” to kernel namespaceVincent Laporte
2019-02-25Merge PR #9620: Stdlib HTML documentation: fix a few absolute URLsThéo Zimmermann
Reviewed-by: Zimmi48
2019-02-25Merge PR #9511: Enable whitespace checking for some forgotten files.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-25[Gitlab-CI] Deploy api documentation to GH-PagesVincent Laporte
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
Supersedes #8718.
2019-02-22Merge PR #9364: Apply implicit binders to Hypothesis inside sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22Merge PR #9576: [library] Remove `-boot` option.Enrico Tassi
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-22Merge PR #9561: [dev] Add include versions for Dune builds.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22Merge PR #9539: [coqdoc] Add the From keywordGaëtan Gilbert
Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 11:44:57 +0000