aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-06replace RList by list RYves Bertot
add an overlay for coquelicot remove functions from RList: In, Rlength, cons_Rlist, app_RList because they are essentially the same as In, length, app, and map from List (beware that the order of arguments changes for map, and the In function contains reversed equalities). adds deprecation warnings for Rlist and Rlength adds deprecated notations for RList.cons and RList.nil
2020-02-06Merge PR #11458: Don't install doc_grammarEnrico Tassi
2020-02-06Merge PR #11478: Nicer kernel universe error for inductivesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-06Merge PR #10835: Accepting a few more variants of format for recursive ↵Pierre-Marie Pédrot
notations (+ a fix about locations) Reviewed-by: ppedrot
2020-02-05Merge PR #11414: Remove the Tactic menu from CoqIDE.Hugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2020-02-05Merge PR #11511: Delay lifting in Evarsolve aliasing.Enrico Tassi
Reviewed-by: gares
2020-02-04Merge PR #11491: Small side effect cleanupPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-02-04Merge PR #11513: Test for #5617: Primitive projections confuse the ↵Gaëtan Gilbert
termination checker. Reviewed-by: SkySkimmer
2020-02-04Merge PR #11514: add regression test for liaPierre-Marie Pédrot
Reviewed-by: fajb
2020-02-04Merge PR #11474: Fix efficiency regression #11436Vincent Laporte
Ack-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: vbgl
2020-02-03add regression test for liaAndres Erbsen
2020-02-03Merge PR #11508: [ci] [fiat-crypto] Use the pinned bedrock2Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-03Test for #5617: Primitive projections confuse the termination checker.Pierre-Marie Pédrot
Fixes #5617.
2020-02-03Do not return a full term in Evarsolve alias expansion.Pierre-Marie Pédrot
The only user is merely observing whether this can be an rel / var alias.
2020-02-03Delay lifting in Evarsolve aliasing.Pierre-Marie Pédrot
It turns out that eagerly computing the lift of huge terms when it is not used is not great for performance. Fixes part of #11488.
2020-02-03Merge PR #11497: [opam] Don't disable native compute in opam.dev fileGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-03Merge PR #11493: [makefile] Ignore _build_boot directoryGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-03Fix efficiency regression #11436Frédéric Besson
- The cutting plane has been (sometimes) improved to generate stronger cuts. - There is now some support for profiling the Simplex see documentation for Show Lia Profile.
2020-02-03Merge PR #11481: Do not rely on Libobject for the current environment in ↵Maxime Dénès
extraction. Reviewed-by: maximedenes
2020-02-03Merge PR #11490: [exn] Don't reraise in exception printersPierre-Marie Pédrot
Ack-by: aspiwack Reviewed-by: ppedrot
2020-02-02[ci] [fiat-crypto] Use the pinned bedrock2Jason Gross
Fiat-Crypto does not guarantee compatibility with the tip of bedrock2, only with the pinned version, and bedrock2 is still relatively unstable. So we make the CI not have Fiat-Crypto depend on bedrock2, and instead use the pinned submodule, by using `EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1` rather than `EXTERNAL_DEPENDENCIES=1`.
2020-02-02Merge PR #11500: [ci] [fiat-crypto-legacy] Use new, faster targetsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-02Merge PR #11484: Fix 11483 (Performance bug of PrimFLoat.compare with ↵Pierre-Marie Pédrot
native_compute) Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-02Merge PR #11326: Refactoring part of #11120 about printing applied global ↵Emilio Jesus Gallego Arias
references Reviewed-by: ejgallego
2020-02-02Merge PR #11466: checkdeps.py: add missing dep & report deps all at onceThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-31[ci] [fiat-crypto-legacy] Use new, faster targetsJason Gross
The computation of which files to build is now mostly cached rather than computed, eliminting basically all of the wait-time from `make` to the first invocation of `coqc`. Note that we no longer need to invoke `./etc/ci/remove_autogenerated.sh`, but it does not hurt, and it speeds up `coqdep` somewhat significantly. Fixes #9298
2020-01-31More tolerant in format for recursive notations.Hugo Herbelin
This is probably a bit overkill but users are tempted to experiment it, so we accept that both ends of a recursive notation are surrounded with boxes which contain printing hints. The alternative would have been to forbid the ends of a recursive notation to be in boxes, but strictly speaking it is a bit more restricting, even if I don't see a realistic use of the general form.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:37:49 +0000