aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-02-08Merge PR#393: Replace Typeops with Fast_typeopsMaxime Dénès
2017-02-07Revert "Extraction: avoid deprecated functions of module String"Pierre Letouzey
2017-02-07Extraction cosmetic: no whitespaces in printing empty modulesPierre Letouzey
2017-02-07Extraction: remove the "print to devnull" hack now that pp isn't lazy anymorePierre Letouzey
2017-02-07Extraction: avoid deprecated functions of module StringPierre Letouzey
2017-02-07Extraction: simplify the generated code for difficult name conflictsPierre Letouzey
2017-02-07Extraction : get_duplicates (via option) instead of check_duplicates (via Not...Pierre Letouzey
2017-02-07configure: avoid deprecated warningsPierre Letouzey
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
2017-02-07Merge PR#425: [travis] [External CI] [geocoq] don't build slow fileMaxime Dénès
2017-02-07[travis] [External CI] [geocoq] don't build slow fileEmilio Jesus Gallego Arias
2017-02-07Merge PR#424: [travis] [External CI] iris-coq: fix dependenciesMaxime Dénès
2017-02-07[travis] [External CI] iris-coq: fix dependenciesEmilio Jesus Gallego Arias
2017-02-07Merge PR#421: [travis] Perform parallel testingMaxime Dénès
2017-02-07[travis] [External CI] GeoCoqEmilio Jesus Gallego Arias
2017-02-07[travis] Enable 32bit test-suite + validate.Emilio Jesus Gallego Arias
2017-02-07[travis] Move ci files from `tools` to `dev`.Maxime Dénès
2017-02-07[travis] [External CI] C-Corn color coquelicot cpdt fiat-crypto floqc iris-co...Emilio Jesus Gallego Arias
2017-02-07[travis] [External CI] Script renaming.Emilio Jesus Gallego Arias
2017-02-07[travis] Improvements to main scriptEmilio Jesus Gallego Arias
2017-02-07[travis] [External CI] compcert HoTT math-compEmilio Jesus Gallego Arias
2017-02-06[travis] Run tests using a parallel matrix.Emilio Jesus Gallego Arias
2017-02-06Merge PR#419: [travis] CoqIde + doc + last available LSTMaxime Dénès
2017-02-04[travis] : more apt deps + parallel jobs + non-container basedPierre-Yves Strub
2017-02-04[travis] CoqIde + doc + last available LSTPierre-Yves Strub
2017-02-03Merge PR#418: Travis CI configurationMaxime Dénès
2017-02-03Travis CI configuration. Runs validate & test-suite.Pierre-Yves Strub
2017-02-01Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-01Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2017-01-31Fixing #5311 (anomaly on unexpected intro pattern).Hugo Herbelin
2017-01-30Merge PR#408: [native comp] Improve error message on linking error.Maxime Dénès
2017-01-30Fix a typo in STM universe communications.Maxime Dénès
2017-01-30Merge PR#355: Remove unused feedback_content: GoalsMaxime Dénès
2017-01-28Fix bug #5262: Error should tell me which name is duplicated.Pierre-Marie Pédrot
2017-01-28Remove useless commentsGaetan Gilbert
2017-01-27Fix documentation typos.Guillaume Melquiond
2017-01-26Adding a printer for Proof.proof reflecting the focusing layout.Hugo Herbelin
2017-01-26[native comp] Improve error message on linking error.Emilio Jesus Gallego Arias
2017-01-26Fixing #5326 (anomaly on some unsupported case of 'pat).Hugo Herbelin
2017-01-24Merge PR#383: fix #5244: set printing width ignored when given enough spaceMaxime Dénès
2017-01-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2017-01-23Fixing unification regression #5323.Hugo Herbelin
2017-01-22Adding a new evar source to remember the name of evars which wereHugo Herbelin
2017-01-22Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).Hugo Herbelin
2017-01-21Revert "Process Next Obligation proofs in parallel (fix #5314)"Enrico Tassi
2017-01-20Process Next Obligation proofs in parallel (fix #5314)Enrico Tassi
2017-01-20Do not add redundant side effects in tactic code.Pierre-Marie Pédrot
2017-01-19Merge branch 'v8.6'Pierre-Marie Pédrot
2017-01-17Mapping named_context_val preserves sharing when possible.Pierre-Marie Pédrot
2017-01-17STM: fix run-time classification of VernacInstance (fix #5313)Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 19:21:30 +0000