aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-30Merge PR #11464: Fix off-by-one in docs of `first num last` (fix #11463)Enrico Tassi
Reviewed-by: gares
2020-01-30Merge PR #11418: Add some more info to the maintainer doc.Maxime Dénès
Reviewed-by: maximedenes
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
Reviewed-by: maximedenes
2020-01-30Merge PR #11480: Remove unused CEphemeron.iter_opt, cleanup commentsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-30Merge PR #11409: [rfc] [mltop] Removal of dynamic loading of object and ↵Pierre-Marie Pédrot
`.ml` files Ack-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2020-01-30Remove unused CEphemeron.iter_opt, cleanup commentsGaëtan Gilbert
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
This seems seldom used and I think in general instrumentation this way is pretty limited (usually better to use the build system to tweak) It thus seems worth removing as to simplify `Mltop` a bit, but of course comments are welcome.
2020-01-29Nicer kernel universe error for inductivesGaëtan Gilbert
Not sure if it's possible to see it without a plugin.
2020-01-29Merge PR #11399: Checker: use inductive's check_template flagPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-29Merge PR #11408: [mltop] Remove error handling hacks in favor of default ↵Pierre-Marie Pédrot
methods. Reviewed-by: ppedrot
2020-01-29Merge PR #11455: Small API additions to kernel/univPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-29Merge PR #11472: Fix #11467 ('e' was not displayed when printing decimal ↵Pierre-Marie Pédrot
notations in R) Reviewed-by: erikmd Reviewed-by: ppedrot
2020-01-29Merge PR #11473: Remove dead code in Globnames.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-29Merge PR #11469: Add reduction-effects to the CIGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-28Add reduction-effects to the CIJason Gross
2020-01-28docs: Update release-process.md about opam/docker packagingErik Martin-Dorel
* Add hyperlinks
2020-01-28docs: Add missing prefix (bug_*.v)Erik Martin-Dorel
Related: https://github.com/coq/coq/pull/8630
2020-01-28Fix #11467Pierre Roux
'e' was not displayed when printing decimal notations in R : Require Import Reals. Check (1.23e1, 32e+1, 0.1)%R. was giving < (123-1%R, 321%R, 1-1%R) instead of < (123e-1%R, 32e1%R, 1e-1%R) This was introduced in #8764 (in Coq 8.10).
2020-01-28Merge PR #11376: Fix fold order in CArray.fold_right(2)_mapPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-28Remove dead code in Globnames.Pierre-Marie Pédrot
2020-01-28Merge PR #11379: [ocaml] Remove Custom Backtrace module in favor of OCaml'sPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-28Merge PR #11419: schemes: use rigid universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-28Merge PR #11459: cleanup: Lib.freeze doesn't use its [~marshallable] argumentMaxime Dénès
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes
2020-01-27Rephrase to reduce ambiguityPaolo G. Giarrusso
This is the smallest possible change to clarify the text without making it even more formal.
2020-01-27Fix off-by-one in docs of `first num last` (fix #11463)Paolo G. Giarrusso
2020-01-27checkdeps.py: report *all* missing dependencies at oncePaolo G. Giarrusso
Otherwise you need a few feedback loops to install all dependencies.
2020-01-27checkdeps: check for sphinxcontrib-bibtexPaolo G. Giarrusso
I lacked this package, and got: ``` $ make -j2 COQ_USE_DUNE=1 refman-html [...] env doc/sphinx_build (exit 2) (cd _build/default/doc && /usr/bin/env COQLIB=.. sphinx-build -j4 -W -b html -d sphinx_build/doctrees sphinx sphinx_build/html) Running Sphinx v2.1.2 Extension error: Could not import extension sphinxcontrib.bibtex (exception: No module named 'sphinxcontrib.bibtex') make: *** [refman-html] Error 1 ```
2020-01-27cleanup: Lib.freeze doesn't use its [~marshallable] argumentGaëtan Gilbert
2020-01-27Checker: use inductive's check_template flagGaëtan Gilbert
And enable related test.
2020-01-27Merge PR #11415: Remove the CoqIDE "Revert all Buffers" command.Hugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2020-01-27schemes: use rigid universesGaëtan Gilbert
so for instance ~~~coq Set Printing All. Set Printing Universes. Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . Lemma bla@{u v|u < v} : foo@{u v} -> False. Proof. induction 1. Qed. ~~~ works.
2020-01-27Fix fold order in CArray.fold_right(2)_mapGaëtan Gilbert
These functions are unused in Coq itself but this may break some plugins. Close #10987
2020-01-27Small API additions to kernel/univGaëtan Gilbert
- allow viewing the internal representation of uglobal and universe (with universe, this replaces the "map" function. I kept exists and for_all as they felt somewhat convenient) - add universe set and map modules (currently unused but they're natural)
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: maximedenes
2020-01-25Publishing a new version on Zenodo: not a relevant step for beta versions.Théo Zimmermann
Also, stop pinging when copying checklist to new issue.
2020-01-23Merge PR #11446: Changed Gitlab CI runner tag for Windows to windows-inriaEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-01-23Changed Gitlab CI runner tag for Windows to windows-inriaMichael Soegtrop
2020-01-23Merge PR #11444: Minor tweaks to the 8.11 changelog.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2020-01-23Merge PR #11445: Clear patches folder before each windows build runThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-23More minor tweaks to the 8.11 changelog.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-01-23Add missing 'and'.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-01-22Clear patches folder before each windows build runMichael Soegtrop
2020-01-22Minor tweaks to the 8.11 changelog.Théo Zimmermann
2020-01-22Add explicit types to changelog entries.Théo Zimmermann
2020-01-22Fix typo in changelog entry.Théo Zimmermann
2020-01-22Merge PR #11372: Changelog for 8.11.0.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-22Merge PR #11438: [lint] Use makefile wrapper instead of calling dune command ↵Théo Zimmermann
directly. Reviewed-by: Zimmi48
2020-01-22Insert changelog entry for #11430 from v8.11 branch.Théo Zimmermann
2020-01-22[lint] Use makefile wrapper instead of calling dune command directly.Emilio Jesus Gallego Arias
This is necessary until we get of the voboot step. See https://github.com/coq/coq/pull/11406#issuecomment-577261843 for more details.
2020-01-22Move new entries in 8.11.0 changelog.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 21:38:01 +0000