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-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-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.
2019-04-02Add overlaysPierre Roux
2019-04-02Allow underscores as comments in numeral constants.Pierre Roux
The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)?
2019-04-02Update documentationPierre Roux
2019-04-02Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)Pierre Roux
2019-04-02Make R parser parse decimals (e.g., 1.02e+01)Pierre Roux
RealField.v is slightly modified so that the ring/field tactics consider the term (IZR (Z.pow_pos 10 _)) produced when parsing exponents as constants.
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
Rather than integers '[0-9]+', numeral constant can now be parsed according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'. This can be used in one of the two following ways: - using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin - using `Numeral Notation` with the type `decimal` added to `Decimal.v` See examples of each use case in the next two commits.
2019-04-02Rename raw_natural_number to raw_numeralPierre Roux
In anticipation of an extension from natural numbers to other numeral constants.
2019-04-02Rename the INT token to NUMERALPierre Roux
In anticipation of future uses of this token for non integer numerals.
2019-04-01Replace type sign = bool with SPlus | SMinusPierre Roux
2019-04-01Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and ↵Vincent Laporte
#9615) Reviewed-by: Zimmi48 Ack-by: fajb Reviewed-by: vbgl
2019-04-01Merge PR #9874: [interp] [numeral] Improve numeral notations to support Ind ↵Emilio Jesus Gallego Arias
and to not use the VM Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-04-01Merge PR #9880: [CI] Coquelicot: use development version and disable on WindowsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 05:14:18 +0000