aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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...
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-02 23:59:04 +0000