aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2019-04-01[doc] Add a note about Dune support to the manual.Emilio Jesus Gallego Arias
2019-04-01Update numeral notation printing docJason Gross
Fixes #9844
2019-04-01Update CHANGESJason Gross
2019-04-01Add test-case for #9840Jason Gross
2019-04-01[numeral] Add a case for IndRef in constr_of_globJason Gross
Fixes #9840
2019-04-01[interp] [numeral] Use cbv rather than vmJason Gross
It is important to fully normalize the term, *including inductive parameters of constructors*; see https://github.com/coq/coq/issues/9840 for details on what goes wrong if this does not happen, e.g., from using the vm rather than cbv. Supersedes / closes #9655
2019-04-01[CI] Disable Coquelicot on WindowsVincent Laporte
2019-04-01[CI] Coquelicot: use “master” development versionVincent Laporte
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:37:28 +0000