aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-10Functionalize env in type classesMaxime Dénès
I had to reorganize the code a bit. The Context command moved to comAssumption, as it is not so related to type classes. We were able to remove a few hooks on the way.
2019-04-10Move vernac-related part of coercions to vernacMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
One other call still remains, but will require to refactor some section-handling code.
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-04-10Fix constant order in heads.mlMaxime Dénès
As per the OCaml documentation, the order for maps should be total. I also remove some circumvolutions that were added around eliminators and canonical names because of this incorrect order.
2019-04-10Merge PR #9941: Improve SProp error message to mention the Allow StrictProp ↵Gaëtan Gilbert
flag. Reviewed-by: SkySkimmer
2019-04-10Improve SProp error message to mention the Allow StrictProp flag.Théo Zimmermann
And document the error message.
2019-04-09Merge PR #9928: Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.Enrico Tassi
Reviewed-by: gares
2019-04-09Merge PR #9931: Fix spelling in comment.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-08Fix spelling in comment.nlewycky
Fix spelling (French fonction --> English function).
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-08Merge PR #9915: Remove cache in HeadsEnrico Tassi
Reviewed-by: gares
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-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-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 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-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-02CI: Use job-local timeout for build-template and test-suite-templateGaëtan Gilbert
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 PR #9659: Fix #9652: rewrite fails to detect lack of progressEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-04-02Document the Fast Name Printing option.Pierre-Marie Pédrot
2019-04-02Fast name generation in detyping.Pierre-Marie Pédrot
We provide a flag that allows for a dumber but O(log n) algorithm generating fresh names in detyping.
2019-04-02Define an efficient representation of subscripted identifiers.Pierre-Marie Pédrot
This is not used yet but it will become useful for efficiently generate fresh identifiers.
2019-04-02Abstract away the name generation algorithm in Detyping.Pierre-Marie Pédrot
For now it does not change anything, but it will make the move towards a faster algorithm seamless.
2019-04-02Pass flags through a record in Detyping.Pierre-Marie Pédrot
There was a hidden bug to an unexpected variable capture in decomp_branch. Let us use proper structures to avoid this kind of mess.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:55:24 +0000