aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-08Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.Pierre-Marie Pédrot
Unfortunately, the only sane fix I was able to hack was to deactivate the possibility to change the background colour altogether. Trying to do otherwise is a real Pandora's box which is ultimately triggered by the lack of lablgtk3 bindings for the GtkStyleContext class. I tried a lot of alternative approaches, to no avail. This includes catching the selection signal, reimplementing selection by hand in GtkTextView, and even reading the internal details of the GTK implementation turned not that helpful. For the time being (8.10 beta) I think we do not have much choice.
2019-04-08Don't store closures in summary (reduction effects)Gaëtan Gilbert
We already have indirection (constant -> effect name, effect name -> function) so we only need to stop using summary.ref for the second map.
2019-04-08Merge PR #9915: Remove cache in HeadsEnrico Tassi
Reviewed-by: gares
2019-04-08coq_makefile install target: error if any file is missingGaëtan Gilbert
2019-04-08Merge PR #9900: [native compiler] Fix critical bug with stuck primitive ↵Pierre-Marie Pédrot
projections Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-06Merge PR #9924: Fix numeral notations test in async mode.Emilio Jesus Gallego Arias
2019-04-06Fix numeral notations test in async mode.Gaëtan Gilbert
Async causes output reordering in one test. Since we don't care about the output of that test (it's just a [Fail]) we move it to success/.
2019-04-06Merge PR #9923: [ci/deploy] Fix branch creation when pushing to ↵Emilio Jesus Gallego Arias
coq/coq-on-cachix. Reviewed-by: ejgallego
2019-04-06Fix pretty-printing of primitive integersErik Martin-Dorel
A scope delimiter was missing for primitive integers constants. Add related regression tests.
2019-04-06[ci/deploy] Fix branch creation when pushing to coq/coq-on-cachix.Théo Zimmermann
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
Since e1e7888, stuck projections were not computed correctly. Fixes #9684
2019-04-05[native compiler] Normalize before destructuring sortMaxime Dénès
This was making an assertion fail on https://github.com/coq/coq/issues/9684 after 23f84f37
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
We perform some cleanup and remove dependency of `proofs/` on `interp/`, which seems logical. In fact, `interp` + `parsing` are quite self-contained, so if there is interest we could also make tactics to depend directly on proofs.
2019-04-05Merge PR #9685: [vernac] Small cleanup to remove assert false.Vincent Laporte
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: vbgl
2019-04-05Remove cache in HeadsMaxime Dénès
This cache makes the pretyper depend on components that should morally be higher-level (Libobject and co), so I'd like to see how critical this cache is before taking any action.
2019-04-05Merge pull request coq/ltac2#116 from proux01/master-parsing-decimalPierre-Marie Pédrot
[coq] Adapt to coq/coq#8764
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01
2019-04-04Update CHANGES.mdPierre Roux
2019-04-04Adapt to coq/coq#8764Pierre Roux
2019-04-04Merge PR #9904: [CI] Fix build of math-comp dependenciesGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-04-04[CI] Fix build of math-comp dependenciesMaxime Dénès
We were incorrectly calling the global `install` target even when building only subcomponents of the library.
2019-04-04Merge PR #9901: [dune] Fix include object dirs.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-04[dune] Fix include object dirs.Emilio Jesus Gallego Arias
In Dune >= 1.8 object dirs have changed; this should be stable for a while, however we want a more robust setup for sure, which I think it should be able to be implemented when we have a single build system.
2019-04-04Merge PR #9881: Protect some I/O routines from SIGALRMEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: maximedenes
2019-04-03Merge PR #9890: Improve coqchk -norec perf by not checking for ill-formed ↵Pierre-Marie Pédrot
data in dependencies Reviewed-by: ppedrot
2019-04-03Merge PR #9804: CI: Use job-local timeout for build-template and ↵Emilio Jesus Gallego Arias
test-suite-template Reviewed-by: ejgallego Reviewed-by: gares
2019-04-03Merge PR #9861: [program] Allow evars in type of fixpoints.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-04-03Protect some I/O routines from SIGALRMMaxime Dénès
This is necessary to prevent Coq from sending ill-formed output in some scenarios involving `Timeout`. Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2019-04-03Merge PR #9078: Provide a faster bound name generation algorithm through a flagVincent Laporte
Ack-by: jfehrle Ack-by: ppedrot Reviewed-by: vbgl
2019-04-03Merge PR #9896: Minor correction to numeral notations docThéo Zimmermann
Reviewed-by: Zimmi48
2019-04-03Merge PR #8638: Remove -compat 8.7Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: jfehrle Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-03Minor correction to numeral notations docJason Gross
2019-04-02Merge PR #9668: Consolidate credits and changelog information in a single place.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: vbgl
2019-04-02[ssr] rewrite takes optional function to make the new valued of the redexEnrico Tassi
2019-04-02[ssr] implement "under i: ext_lemma" by rewrite ruleEnrico Tassi
Still to do: renaming the bound variables afterwards
2019-04-02[ssr] under: Add opaque modules for tagging and notation supportErik Martin-Dorel
(Note: coq notations cannot contain \n) Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2019-04-02[ssr] fix implementation of refine ~first_goes_lastEnrico Tassi
2019-04-02[ssr] clean up type declaration of ssrrewritetacEnrico Tassi
2019-04-02[ssr] move is_ind/constructor_ref to ssrcommonEnrico Tassi
2019-04-02[ssr] under: rewrite takes an optional bool argErik Martin-Dorel
* If this flag under=true: enable flag with_evars of refine_with to create evar(s) if the "under lemma" has non-inferable args. * Backward compatibility of ssr rewrite is kept. * Fix test-suite/ssr/dependent_type_err.v
2019-04-02CI: Use job-local timeout for build-template and test-suite-templateGaëtan Gilbert
2019-04-02Merge pull request coq/ltac2#118 from vbgl/rm-hardwired-hint-dbPierre-Marie Pédrot
Fix for https://github.com/coq/coq/pull/8984
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
2019-04-02coqchk: use unsafe marshal for dependencies of -norec librariesGaëtan Gilbert
on test-suite/arithmetic/mod: 2.6s to 0.45s
2019-04-02coqchk: don't marshal opaques for dependencies of -norec librariesGaëtan Gilbert
About 20% better perf on test-suite/arithmetic/mod (3.4s to 2.6s)
2019-04-02coqchk: do not validate dependencies of -norec librariesGaëtan Gilbert
For instance this halves the time it takes to check the test-suite/arithmetic/ files. on mod: 7.5s to 3.4s
2019-04-02Remove -compat 8.7Jason Gross
This removes various compatibility notations. Closes #8374 This commit was mostly created by running `./dev/tools/update-compat.py --release`. There's a bit of manual spacing adjustment around all of the removed compatibility notations, and some test-suite updates were done manually. The update to CHANGES.md was manual.
2019-04-02Merge PR #9875: [doc] Add a note about Dune support to the manual.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-02Merge pull request coq/ltac2#117 from ejgallego/opam_updatePierre-Marie Pédrot
[opam] Update file to newer format and build system.
2019-04-02[opam] Update file to newer format and build system.Emilio Jesus Gallego Arias
Using Dune in the OPAM file does allow to use some goodies such as `dune-release` etc...
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-26 03:23:46 +0000