aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-23Fix the information of the level of ; vs ; [ ]Théo Zimmermann
2019-01-23Improve the note in the beginning of the Ltac chapter.Théo Zimmermann
In particular, add an example to illustrate the associativity of ;
2019-01-23Merge PR #9361: Make prvect tail recursive (fix #9355)Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-01-23Merge PR #9382: Transfer maintenance of appveyor infrastructure to the CI teamThéo Zimmermann
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-01-23Merge PR #9239: [ci] [appveyor] Pass -j2 to Appveyor's build and build test ↵Maxime Dénès
suite again
2019-01-22Transfer maintenance of appveyor infrastructure to the CI teamMaxime Dénès
2019-01-22Merge PR #9225: Fix issue: Windows CI: cygwin install cache is not reused #9212Maxime Dénès
Reviewed-by: maximedenes
2019-01-22Merge PR #9308: Remove outdated gitignore coqprojectfile.mlEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-01-22Merge PR #9332: Add OSX job to azureEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-01-22Make prvect tail recursive (fix #9355)Gaëtan Gilbert
Using a unit test as it's way faster than messing with universes. You can test with universes by ~~~coq Set Universe Polymorphism. Definition x1@{i} := True. Definition x2 := x1 -> x1. Definition x3 := x2 -> x2. Definition x4 := x3 -> x3. Definition x5 := x4 -> x4. Definition x6 := x5 -> x5. Definition x7 := x6 -> x6. Definition x8 := x7 -> x7. Definition x9 := x8 -> x8. Definition x10 := x9 -> x9. Definition x11 := x10 -> x10. Definition x12 := x11 -> x11. Definition x13 := x12 -> x12. Definition x14 := x13 -> x13. Definition x15 := x14 -> x14. Definition x16 := x15 -> x15. Definition x17 := x16 -> x16. Definition x18 := x17 -> x17. Definition x19 := x18 -> x18. About x19. (* 262144 universes *) ~~~ Note on my machine `About x18.` did not overflow even before this commit.
2019-01-21Merge PR #9027: Refactor checking of inductive typesMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: mattam82 Ack-by: maximedenes Ack-by: ppedrot
2019-01-21Add OSX job to azureGaëtan Gilbert
2019-01-21Refactor typechecking of inductive typesGaëtan Gilbert
We split into smaller functions, use more specific types for universe manipulation, and try to limit how much of the big tuple gets passed to subroutines.
2019-01-21Move inductive typecheck to file independent from positivity check.Gaëtan Gilbert
This is strictly code movement.
2019-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2019-01-21Merge PR #9304: Default disable auto template warning.Maxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-01-21Merge PR #9340: Add badges linking to a selection of up-to-date Coq packages.Maxime Dénès
Reviewed-by: maximedenes
2019-01-20Merge PR #9353: Fix merge-pr.sh when multiple review commentsMaxime Dénès
Reviewed-by: maximedenes
2019-01-17Fix merge-pr.sh when multiple review commentsGaëtan Gilbert
It used to output duplicate trailers.
2019-01-17Merge PR #9326: [ci] compile with -quick & validate after vio2voGaëtan Gilbert
Reviewed-by: ejgallego Ack-by: SkySkimmer Ack-by: gares Ack-by: ppedrot
2019-01-17Merge PR #9345: [ci] Update fiat-crypto to the new pipelineGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-01-17Merge PR #9192: Issue #9175, #9190, #9191 (various minor Windows build issues)Maxime Dénès
Reviewed-by: Zimmi48
2019-01-17Merge PR #9048: Fix vernac classification of `Fail Instance`Enrico Tassi
Reviewed-by: gares
2019-01-17Merge PR #9242: merge-pr: add reviewer info to commit messageMaxime Dénès
Reviewed-by: maximedenes Ack-by: ejgallego
2019-01-16Merge PR #9346: Add .nia.cache to .gitignoreGaëtan Gilbert
2019-01-16Add .nia.cache to .gitignoreJason Gross
2019-01-16[ci] Update fiat-crypto to the new pipelineJason Gross
We're recently reorganized fiat-crypto. This should fix the OOM CI issues. Fixes #9338
2019-01-14Merge PR #9307: Handle local definitions in implicit arguments of InstanceMaxime Dénès
2019-01-13Add badges linking to a selection of up-to-date Coq packages.Théo Zimmermann
The badges displaying the latest packaged version are provided by Repology. The goal is to put forward the packages that are well maintained (updated quickly after a new release) and thus recommended. The history of package updates can be found at: https://repology.org/metapackage/coq/history opam is missing because Repology is not currently tracking opam, but this could be fixed (Repology does not only track Linux-distributions-like package repositories, it also includes programming language package repositories such as CPAN, CRAN, Hackage, RubyGems, and Stackage, thus opam could be added as well).
2019-01-13Refactor badges in README.Théo Zimmermann
2019-01-11[STM] set the mtime of files generated via vio2vo (fix #9334)Enrico Tassi
2019-01-11Fix vernac classification of `Fail Instance`Maxime Dénès
AFAIK `Fail Instance` cannot open a goal.
2019-01-11Merge pull request #8778 from SkySkimmer/merge-plugin-tutoYves Bertot
Move plugin tutorial to Coq repo
2019-01-10Merge PR #9335: [STM] kill no_safe_id anomalyMaxime Dénès
2019-01-10[ci] compile with -quick & validate after vio2voEnrico Tassi
2019-01-10[vio] free resources (file descriptors) as soon as a worker endsEnrico Tassi
2019-01-10[make] support for QUICKEnrico Tassi
The variable QUICK enables the quick compilation chain: - all v files are compiled with -quick to vio files (also -native-compiler no, since it is quicker) - then all vio files are turned to vo files $NJOBS at a time All occurrences of .vo use now .$(VO) that can be either .vo or .vio depending of QUICK being defined. Targets that only make sense for .vo files have to use $(VAR:.$(VO)=.vo)
2019-01-10[STM] kill no_safe_id anomalyEnrico Tassi
2019-01-10Merge PR #9143: Documenting the internal role of to_string and print in NamesMaxime Dénès
2019-01-10Merge PR #9331: [STM] Fix semantics of `cur_id` w.r.t. error statesEnrico Tassi
2019-01-10[checker] avoid some printing in non verbose modeEnrico Tassi
2019-01-09[STM] Fix semantics of `cur_id` w.r.t. error statesMaxime Dénès
2019-01-09Merge PR #9318: Add Azure Pipelines build badgeThéo Zimmermann
2019-01-09Merge PR #9327: [Manual] Remove link to non-existing CSS fileClément Pit-Claudel
2019-01-09Merge PR #9088: Add CI job running test suite with `async-proofs on`Emilio Jesus Gallego Arias
2019-01-09[Manual] Remove link to non-existing CSS fileVincent Laporte
2019-01-09Merge PR #9322: [ci] Update fiat-crypto legacyGaëtan Gilbert
2019-01-09Make some tests more robust by adding missing proof terminatorsMaxime Dénès
2019-01-09Test ltacprof in sequential modeMaxime Dénès
Scripting these commands in async mode does not really make sense.
2019-01-09Add a CI job running test suite with `-async-proofs on`Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:17:23 +0000