aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-01-21At Qed, if shelved goals remain, emit a warning instead of an errorMaxime Dénès
2019-01-21[EConstr] Expose API to normalize and check if evars are remainingMaxime Dénès
2019-01-21Merge PR #9304: Default disable auto template warning.Maxime Dénès
2019-01-21Merge PR #9340: Add badges linking to a selection of up-to-date Coq packages.Maxime Dénès
2019-01-20Merge PR #9353: Fix merge-pr.sh when multiple review commentsMaxime Dénès
2019-01-19Fix makefile .merlin for unit testsGaëtan Gilbert
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
2019-01-19Fix recursive loadpath of ML filesMaxime Dénès
2019-01-18[ssr] compile "=> {x..}/v" as "/v{x..v}"Enrico Tassi
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
2019-01-18[ssr] clean up implementation of {}/v -> /v{v}Enrico Tassi
2019-01-17Fix merge-pr.sh when multiple review commentsGaëtan Gilbert
2019-01-17Merge PR #9326: [ci] compile with -quick & validate after vio2voGaëtan Gilbert
2019-01-17Merge PR #9345: [ci] Update fiat-crypto to the new pipelineGaëtan Gilbert
2019-01-17Merge PR #9192: Issue #9175, #9190, #9191 (various minor Windows build issues)Maxime Dénès
2019-01-17Merge PR #9048: Fix vernac classification of `Fail Instance`Enrico Tassi
2019-01-17Merge PR #9242: merge-pr: add reviewer info to commit messageMaxime Dénès
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
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
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
2019-01-11Merge pull request #8778 from SkySkimmer/merge-plugin-tutoYves Bertot
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
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-09Stop [Print] from saying [is (not) universe polymorphic].Gaë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
2019-01-09Add a CI job running test suite with `-async-proofs on`Maxime Dénès
2019-01-09Make it possible to pass flags to coq when running test suiteMaxime Dénès
2019-01-09Merge PR #9316: Fix #3934: coqc -time -quick gives unreadable outputEnrico Tassi
2019-01-09Merge PR #9273: Fix #9272: `Unset Nested Proofs Allowed` does not capture nes...Enrico Tassi
2019-01-08Move position and update GitLab alt textKayla Ngan
2019-01-08[ci] Update fiat-crypto legacyJason Gross
2019-01-08Fix #3934: coqc -time -quick gives unreadable outputMaxime Dénès