aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-31[opam] Don't disable native compute in opam.dev fileEmilio Jesus Gallego Arias
See discussion in https://github.com/coq/bignums/issues/26 and #11476 We still disable it in developer fast builds as the speed up is considerable, it can be enabled by just calling `./configure`
2020-01-31[makefile] Ignore _build_boot directoryEmilio Jesus Gallego Arias
PR #11267 reverted commit d21e17ac99dfb2008f2e2bfdb373413490d1ffc7 (of PR #10695) by error, this reinstates it.
2020-01-30Factorize export_private_constants + register_side_effectGaëtan Gilbert
2020-01-30[exn] Don't reraise in exception printersEmilio Jesus Gallego Arias
This behaviour seems a bit dubious and it is indeed not needed, also such re-raises seem like they will mess with the backtrace.
2020-01-30export_private_constants doesn't use the [constr in_univ_ctx] argumentGaëtan Gilbert
2020-01-30Notations: Fixing a wrong location in format.Hugo Herbelin
2020-01-30Constrextern.ml: Move a function earlier to be usable for pattern printing.Hugo Herbelin
2020-01-30Minor indentation change.Hugo Herbelin
2020-01-30Refactoring code for matching partial applications against notations.Hugo Herbelin
Should be semantically equivalent.
2020-01-30Refactoring code for externing applications.Hugo Herbelin
Should be semantically equivalent.
2020-01-30Printing tests for applied references combined with impl. args. and notations.Hugo Herbelin
This shows a few bugs and even anomalies. See issue #11091. See further commits for some fixes.
2020-01-30Constrextern.ml: for readability, use auxiliary function for externing records.Hugo Herbelin
2020-01-30Merge PR #11377: coqtop: stop on Sys_blocked_ioEmilio Jesus Gallego Arias
Ack-by: JasonGross Reviewed-by: ejgallego Ack-by: gares
2020-01-30coqtop: stop on Sys_blocked_ioGaëtan Gilbert
Close #10918
2020-01-30Fix 11483Pierre Roux
Performance bug of PrimFLoat.compare with native_compute When adapting Coq.Interval with @erikmd and @silene, we noticed that PrimFLoat.compare is taking a lot of time with native_compute (much more than with vm_compute). This comes from the implementation using the OCaml polymorphic comparison instead of the float comparison.
2020-01-30Don't install doc_grammarGaëtan Gilbert
Fix #11452
2020-01-30Do not rely on Libobject for the current environment in extraction.Pierre-Marie Pédrot
Instead, we export in Safe_typing the current module declaration.
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 04:33:21 +0000