aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-04Remove `unsafe_type_of` from `Coercion`Maxime Dénès
We thread explicitly the evar map everywhere for this purpose.
2020-02-04Apply suggestions from HugoSimonBoulier
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
2020-02-04Correct bug in non max local implicit argumentsSimonBoulier
+ tests in the test-suite for non max local implicit arguments
2020-02-04Non maximal implicits: add overlays for several librariesSimonBoulier
2020-02-04Non maximal implicits: entry in dev/doc/changes.mdSimonBoulier
2020-02-04Add changelog for non maximal implicit argsSimonBoulier
2020-02-04Update doc for non max implicit argumentsSimonBoulier
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-02-04Merge PR #11513: Test for #5617: Primitive projections confuse the ↵Gaëtan Gilbert
termination checker. Reviewed-by: SkySkimmer
2020-02-04Fix #11515: Ltac2 rewrite on wildcard.Pierre-Marie Pédrot
There was an evar leak due to an evarmap not being threaded correctly when computing open terms.
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-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
It was virtually unused except in ssr, and there is no reason to clutter the kernel with irrelevant code. Fixes #9390: What is the purpose of the function "kind_of_type"?
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-02-01No spaces with em-dashes.Théo Zimmermann
Co-Authored-By: Jason Gross <jasongross9@gmail.com>
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-31Clarify expectations for overlays in contributing guide and CI doc.Théo Zimmermann
Contributors are *not* required to prepare all the patches by themselves. They can request help from project authors, who should be ready to take part in this. Also, finish replacing "development" by the more appropriate word "project".
2020-01-31[contributing guide] Clarify some subtitles.Théo Zimmermann
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 18:08:04 +0000