aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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 #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
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
The `-boot` option was used to: - suppress loading of the rc_file - allow to save modules with prefix `Coq` There is no good reason disable saving of modules with `Coq` prefix by default, thus we remove this option. Fixes: #9575
2019-02-22Merge PR #9614: Fix #9613 use -coqlib when invoking coqchkEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-21Merge PR #9588: [azure] [ci] Build on Windows using Dune.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-21Stdlib HTML documentation: fix a few absolute URLsVincent Laporte
2019-02-21Merge PR #9577: [Namegen] Use Global.exists_objlabel in `next_global_ident_away`Pierre-Marie Pédrot
Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-02-21Merge PR #9618: [dev/tools/create_overlays] remove trailing whitespaceEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-21remove meta trailing whitespaceEnrico Tassi
2019-02-21Fix #9613 use -coqlib when invoking coqchkGaëtan Gilbert
In passing add -coqlib to coqchk's usage message.
2019-02-21Merge PR #9388: merge-pr.sh: fix #9387: quick_conf doesn't work in emacs ↵Emilio Jesus Gallego Arias
shell buffer Reviewed-by: ejgallego
2019-02-20Merge PR #9529: Change Primitive message: "is registered" -> "is declared".Vincent Laporte
Reviewed-by: vbgl
2019-02-20Enable whitespace checking for some forgotten files.Gaëtan Gilbert
+ remove checker/.depend forgotten file
2019-02-20Merge PR #9457: Correct W-Ind in Cic description of the reference manual.Théo Zimmermann
Reviewed-by: SkySkimmer
2019-02-20[paths] Try to be more portable on Win32Emilio Jesus Gallego Arias
Absolute paths follow different separator rules so "c:\foo/bar" may not work on `mingw`. We try to improve this situation using OCaml's `Filename.dir_sep/concat`
2019-02-20[azure] [ci] Build on Windows using Dune.Emilio Jesus Gallego Arias
We may want to keep the make-based and Dune job, however the make-based setup is tested by the INRIA workers so it may not be needed. In order for some test to run well, we always run in Dune with an absolute path. The easiest way to get a portable absolute path is to use OCaml itself so we introduce a small executable to do that. While we are at it, we do some cleanup of the test-suite `dune` file, in particular we remove useless comments, set `--no-buffer` so results can be seen in real time, and recognize the `NJOBS` variable as we have moved to a Dune version that supports env vars.
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:15:43 +0000