aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
2020-01-13Merge PR #11285: fix #11279. Specialize h no longer expands letins in the typ...Pierre-Marie Pédrot
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
2020-01-11Merge PR #11367: Minor cleanup of indtypes/indtypingPierre-Marie Pédrot
2020-01-11Merge PR #11349: [refman] [changelog] Announce omega replacement.Pierre-Marie Pédrot
2020-01-10Merge PR #11387: [refman] missing space in "Controlling the locality of comma...Théo Zimmermann
2020-01-10Merge PR #11385: Add badges for Docker Hub and coqorg/coq:latest versionThéo Zimmermann
2020-01-10missing spaceOlivier Laurent
2020-01-10Merge PR #11384: Fix build after merge of #11164Pierre-Marie Pédrot
2020-01-09Merge PR #11371: [merge script] Never bypass outdated branch sanity check.Jason Gross
2020-01-09Add badges for Docker Hub and coqorg/coq:latest versionErik Martin-Dorel
2020-01-09Fix build after merge of #11164Gaëtan Gilbert
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Merge PR #11375: Add note about default goal selector next to bullet docsThéo Zimmermann
2020-01-08Merge PR #11378: let CI test bedrock2's 'tested' branch instead of 'master'Théo Zimmermann
2020-01-08let CI test bedrock2's 'tested' branch instead of 'master'Samuel Gruetter
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
2020-01-08replace deprecated -quick with -vio in the test suiteEnrico Tassi
2020-01-08[refman] [changelog] Announce omega replacement.Théo Zimmermann
2020-01-08Merge PR #11341: Add non-utf8 timing testPierre-Marie Pédrot
2020-01-07[merge script] Never bypass outdated branch sanity check.Théo Zimmermann
2020-01-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
2020-01-07Merge PR #11369: [refman] Correct manual about implicit parameters in inductivesThéo Zimmermann
2020-01-07Merge PR #11317: Fix #11140: Bidirectionality hints perform (surprising?) sim...Enrico Tassi
2020-01-07Correct manual about implicit parameters in inductives.SimonBoulier
2020-01-07cleanup: do not use recargs when computing the reloc table for ctorsGaëtan Gilbert
2020-01-07minor cleanup template_polymorphic_univs: check_levels returns boolGaëtan Gilbert
2020-01-07[coercions] more precise type for coercion tracesMaxime Dénès
2020-01-06doc: mention limitation of bidi hints vs programGaëtan Gilbert
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
2020-01-06Merge PR #11361: Fix #11360: discharge of template inductive with param only ...Pierre-Marie Pédrot
2020-01-06Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx migra...Clément Pit-Claudel
2020-01-06Merge PR #11211: Fixing status reporting for complexity testsGaëtan Gilbert
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2020-01-04Fixing status reporting for complexity tests.Hugo Herbelin
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
2020-01-03Merge PR #11357: coq_makefile: don't use CAMLPKGS when building cmxa of mllibEnrico Tassi
2020-01-03Merge PR #11295: Use code owner teams for every component.Maxime Dénès
2020-01-03coq_makefile: test with CAMLPKGS and mllibGaëtan Gilbert
2020-01-03coq_makefile: don't use CAMLPKGS when building cmxa of mllibGaëtan Gilbert
2020-01-03[tools] Remove support for python2Emilio Jesus Gallego Arias
2020-01-02Merge PR #11335: Stdlib : Arith/Wf_nat : Add statements with output in TypeHugo Herbelin
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
2019-12-31Merge PR #11325: [refman] Add missing s.Pierre-Marie Pédrot
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...Pierre-Marie Pédrot
2019-12-30Merge PR #11345: Remove :flag: that appears in the doc outputThéo Zimmermann
2019-12-29Remove :flag: that appears in the outputJim Fehrle
2019-12-29[refman] Fix bad quoting practice leftover from Sphinx migration.Théo Zimmermann
2019-12-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the Ver...Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 08:21:33 +0000