aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
2019-12-25Show doc notations in boldfaceJim Fehrle
2019-12-24Update merging doc following the full move to teams.Théo Zimmermann
2019-12-24Merge PR #11284: [meta] Add ltac2 information to META.Théo Zimmermann
2019-12-24[meta] Add ltac2 information to META.Emilio Jesus Gallego Arias
2019-12-24[ci] [gitlab] [bedrock] Build bedrock with 1 coreEmilio Jesus Gallego Arias
2019-12-24Merge PR #11316: Windows: switch OCaml to 4.08.1Emilio Jesus Gallego Arias
2019-12-24Add statements with output in TypeOlivier Laurent
2019-12-24[recordops] do not open GlobRefEnrico Tassi
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-12-23Merge PR #11293: Rename files with Class in their name to make their role cle...Hugo Herbelin
2019-12-23Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.Hugo Herbelin
2019-12-23Merge PR #11274: [library] [cleanup] Remove code duplication.Pierre-Marie Pédrot
2019-12-23Windows: switch OCaml to 4.08.1Michael Soegtrop
2019-12-23Merge PR #11324: [refman] Mention Ltac2 in intro.Pierre-Marie Pédrot
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
2019-12-22Use code owner teams for every component.Théo Zimmermann
2019-12-22Apply suggestions from code reviewThéo Zimmermann
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-22[refman] Mention Ltac2 in intro.Théo Zimmermann
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
2019-12-22[refman] Add missing s.Théo Zimmermann
2019-12-22Use a more straightforward algorithm for mulc on 32-bit architectures. (Fixes...Guillaume Melquiond
2019-12-22Simplify equality of 63-bit integers.Guillaume Melquiond
2019-12-22Do not hide constants from the compiler.Guillaume Melquiond
2019-12-21Merge PR #11311: Fix handling of recursive notations with custom entriesHugo Herbelin
2019-12-20Merge PR #11308: Fix complexity test-suite failure reporting on WinEnrico Tassi
2019-12-20Add test cases for #9490 and #9532Maxime Dénès
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès