aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-06unsafe_type_of + match -> sort_of in Tactics.cutGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.change_on_subtermGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.convert_conclGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Eqdecide (2 occurrences)Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Eauto.e_give_exactGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Pretyping.pretype_refGaëtan Gilbert
We already thread the evar map
2020-02-06unsafe_type_of -> type_of in Unification.applyHeadGaëtan Gilbert
We already thread the evar map
2020-02-06unsafe_type_of -> type_of in Tacred.pattern_occsGaëtan Gilbert
This function already returns the evar map so no problem.
2020-02-06unsafe_type_of -> get_type_of in casesGaëtan Gilbert
It goes in an error message so should be fine.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:15:38 +0000