aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-12-19Better error reporting when res is not what is expectedJason Gross
2019-12-19Fix complexity test-suite failure reporting on WinJason Gross
2019-12-19Revert "Fix #11303: skip complexity tests on windows even if bogomips found"Jason Gross
2019-12-19Fix #11303: skip complexity tests on windows even if bogomips foundGaëtan Gilbert
2019-12-18Merge PR #6090: Implement open recursion in the pretyperEnrico Tassi
2019-12-18Merge PR #9786: Fix Equation's ci scriptPierre-Marie Pédrot
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...Pierre-Marie Pédrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
2019-12-18Merge PR #11267: FIND_SKIP_DIRS (make): ignore all dot directoriesEnrico Tassi
2019-12-18Merge PR #11123: Fix signal polling for OCaml 4.10Maxime Dénès
2019-12-18Merge PR #11263: [micromega] fix efficiency regressionMaxime Dénès
2019-12-17Type pretyping is part of the open recursionPierre-Marie Pédrot
2019-12-17Exporting the open-recursion style API.Pierre-Marie Pédrot
2019-12-17Implementing open recursion in the pretyper.Pierre-Marie Pédrot
2019-12-17failwith -> caml_failwithGuillaume Munch-Maccagnoni
2019-12-17Fatal error in VM if SIGINT was seen but no exception occured.Guillaume Munch-Maccagnoni
2019-12-17Fix signal polling for OCaml 4.10Guillaume Munch-Maccagnoni
2019-12-17Merge PR #11299: [VM] fix volatile declarationEmilio Jesus Gallego Arias
2019-12-17[VM] fix volatile declarationGuillaume Munch-Maccagnoni
2019-12-17Merge PR #10762: Fix refine and eapply to mark shelved goals as non-resolvabl...Maxime Dénès
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-12-17Merge PR #11294: Advertise doc for master branch in README.Maxime Dénès
2019-12-16FIND_SKIP_DIRS (make): ignore all dot directoriesGaëtan Gilbert
2019-12-16Merge PR #11291: Being explicit on existence of a remote link in stdlib to av...Théo Zimmermann
2019-12-16Overlay for #11027Gaëtan Gilbert
2019-12-16Advertise doc for master branch in README.Théo Zimmermann
2019-12-16Don't pass (ignored) implicits to interp_mutual_inductive_constrGaëtan Gilbert
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
2019-12-16reduce arguments of template_polymorphism_candidateGaëtan Gilbert
2019-12-16comInductive: remove redundant check_evars callsGaëtan Gilbert
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-16Merge PR #10695: [ci] [dune] Updates to dune builds artifacts.Gaëtan Gilbert