aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-26Add rew dependent NotationsJason 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-22Use the Alloc_small macro from the OCaml runtime rather than our own.Guillaume Melquiond
2019-12-22Centralize the flag handling native compilation.Pierre-Marie Pédrot
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-12-22Export the dynamic type API of libobjects.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
2019-12-20Merge PR #11258: Coherence checking for coercionsEnrico Tassi
2019-12-19Support additional escape sequences in notationsJim Fehrle
2019-12-19Merge PR #11247: Use standard float and integer datatypes in Votour represent...Maxime Dénès
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
2019-12-19Remove trailing \r in complexity measures for WindowsJason Gross