aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-09-29Merge PR #10673: [lemmas] Cleanup users of default proof information.Pierre-Marie Pédrot
2019-09-26Merge PR #10664: Putting sections libstack inside the kernelMaxime Dénès
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-25Clean up InferCumulativity after its move to the kernel.Pierre-Marie Pédrot
2019-09-25Move the Lib section data into the kernel.Pierre-Marie Pédrot
2019-09-25Move cumulativity inference to the kernel.Pierre-Marie Pédrot
2019-09-25Stub code for handling sections in kernel.Pierre-Marie Pédrot
2019-09-25Refine the API to declare section-local universes.Pierre-Marie Pédrot
2019-09-25Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy realsHugo Herbelin
2019-09-25Merge PR #10784: Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindPierre-Marie Pédrot
2019-09-25Merge PR #10781: Fixes #10778 (fresh was not updated after renaming of introp...Pierre-Marie Pédrot
2019-09-24Merge PR #10774: Make `zify` does work for `Z.to_N`Frédéric Besson
2019-09-24Merge PR #10699: [gitlab/ci] Prevent Corn from running if Bignums has failed.Gaëtan Gilbert
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
2019-09-24Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindGaëtan Gilbert
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-23Fixes #10778 (fresh was not updated after renaming of intropattern entry in #...Hugo Herbelin
2019-09-23Merge PR #10776: Fix #10413 (CI failure on tags).Gaëtan Gilbert
2019-09-23Merge PR #10777: Mark SF as allow failure until it gets fixed.Gaëtan Gilbert
2019-09-23Mark SF as allow failure until it gets fixed.Théo Zimmermann
2019-09-23Fix #10413 (CI failure on tags).Théo Zimmermann
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
2019-09-17Merge PR #10738: update elpi to 1.7Gaëtan Gilbert
2019-09-17Merge PR #10476: Remove library-specific code for `Import`.Enrico Tassi
2019-09-17Add changelog entryMaxime Dénès
2019-09-17Overlay for VSTMaxime Dénès
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria
2019-09-16Re-implementation of zifyFrédéric Besson
2019-09-16Optimize multiple importsMaxime Dénès
2019-09-16Optimize `Include`d `Export`sMaxime Dénès
2019-09-16Turn `module_objects` into a recordMaxime Dénès
2019-09-16Add SF overlayMaxime Dénès
2019-09-16Optimize module ExportsMaxime Dénès
2019-09-16Do not cache objects when importing modulesMaxime Dénès
2019-09-16Specialize `ImportObject` to `Export`Maxime Dénès
2019-09-16`do_modtype` -> `load_modtype`Maxime Dénès
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
2019-09-13Merge PR #10748: Hack for fixing #10578: handle between the three main CoqIDE...Pierre-Marie Pédrot
2019-09-13Hack for fixing #10578 (wrong initial handle position separating main windows).Hugo Herbelin
2019-09-12Merge PR #10753: Release notes for 8.10+beta3.Clément Pit-Claudel
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-09-11Merge PR #8567: More general support for installation of coqide keysPierre-Marie Pédrot
2019-09-10Merge PR #10742: Switch maintenance of `ring` to a teamThéo Zimmermann
2019-09-10Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.Hugo Herbelin
2019-09-10Fixing coqide doc about location of "coqiderc" and "coqide.bindings".Hugo Herbelin
2019-09-10CoqIDE: removing option contextual menu on goal, inactive since 2da5db43c.Hugo Herbelin
2019-09-10Moving a standard string function (is_prefix) from Minilib to CString.Hugo Herbelin
2019-09-10Moving configuration of coqide.keys to the coqide executable.Hugo Herbelin
2019-09-10Using GTK+ PRIMARY to factorize CoqIDE keys between MacOS and others.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 23:54:49 +0000