aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-08Avoid hardcoded paths in extractionMaxime Dénès
2020-01-08Avoid warning 40Maxime Dénès
2020-01-08Hide ExtrOcamlStringPlus.v like the other extraction filesXavier Leroy
2020-01-08Support extraction of Coq's string type to OCaml's string type, continuedXavier Leroy
2020-01-08Support extraction of Coq's string type to OCaml's string typeXavier Leroy
2020-01-08Merge PR #11341: Add non-utf8 timing testPierre-Marie Pédrot
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-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
2019-12-29Merge PR #11183: Enhance prodn in .rst doc files to support multiple producti...Théo Zimmermann
2019-12-29Merge PR #11334: Fixes a small bug exposing an _ANONYMOUS_REL in a unificatio...Pierre-Marie Pédrot
2019-12-29Merge PR #10977: Remove the incorrect extra space in Makefile.vofilesEnrico Tassi
2019-12-28Prevent apostrophes and backticks from being stylized in latexJim Fehrle
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-28Merge PR #11323: Fix mulc on 32-bit architecturesMichael Soegtrop
2019-12-28Merge PR #10747: Extend `Print Canonical Projections` with a search functiona...Enrico Tassi
2019-12-28Update doc/sphinx/language/gallina-extensions.rstKazuhiko Sakaguchi
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-27Add critical-bugs entry, tests-suite file, and code comment.Guillaume Melquiond
2019-12-27Merge PR #11315: Ensure that a custom entry cannot be defined twice.Hugo Herbelin
2019-12-27docs: Update changes.rst w.r.t. ssrsetoid.v's simplificationErik Martin-Dorel
2019-12-27fix: Shorten ssrsetoid.vErik Martin-Dorel
2019-12-26Merge PR #11288: [omega] Remove non-documented "omega with *"Théo Zimmermann
2019-12-26Add non-utf8 timing testJason Gross
2019-12-26Merge PR #11336: [ci] [gitlab] [bedrock] Build bedrock with 1 coreThéo Zimmermann
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-26[omega] Remove non-documented "omega with *"Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 11:05:59 +0000