aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-10-07(Partially) Revert "Make Environ.globals abstract."Emilio Jesus Gallego Arias
2019-10-06Merge PR #10834: Fix #10831: minor issues in documentation of Function.Clément Pit-Claudel
2019-10-06Merge PR #10833: 8.10.0 release notes.Vincent Laporte
2019-10-06Fix #10831: minor issues in documentation of Function.Théo Zimmermann
2019-10-068.10.0 release notes.Théo Zimmermann
2019-10-05Changelog for SProp onGaëtan Gilbert
2019-10-05Merge PR #10763: Fix syntax of reduction tactics when listing qualid to reduc...Vincent Laporte
2019-10-05Remove "is_polymorphic_univ" checks in upper layers.Gaëtan Gilbert
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-05Cleanup ComAssumptionGaëtan Gilbert
2019-10-05Move do_primitive from comassumption to its own module.Gaëtan Gilbert
2019-10-05Declare universes for variables outside of Declare.declare_variableGaëtan Gilbert
2019-10-04Improve language.Théo Zimmermann
2019-10-04Merge Direct and Indirect nodes in Opaqueproof.Pierre-Marie Pédrot
2019-10-04Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint data...Pierre-Marie Pédrot
2019-10-04Remove redundancy in section hypotheses of kernel entries.Pierre-Marie Pédrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...Pierre-Marie Pédrot
2019-10-04overlays for sprop default onGaëtan Gilbert
2019-10-04Allow SProp default onGaëtan Gilbert
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive projec...Frédéric Besson
2019-10-03Merge PR #10765: Improved handling of micromega cachesPierre-Marie Pédrot
2019-10-03fix 10765-micromega-caches.rstFrédéric Besson
2019-10-03Merge PR #10727: [library] Move `Declaremods` to `vernac/`Pierre-Marie Pédrot
2019-10-03Improved handling of micromega cachesFrédéric Besson
2019-10-02Merge PR #10809: Postpone the computation of relative constraints in universe...Gaëtan Gilbert
2019-10-02Merge PR #10768: [ci] Update to OCaml 4.09.0, drop now useless "trunk" jobs.Gaëtan Gilbert
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-10-02simplify branch in process_universe_constraintsGaëtan Gilbert
2019-10-02Merge PR #10805: Remove spurious uses of CoInductive in SSR prerequisite.Maxime Dénès
2019-10-02Postpone the computation of relative constraints in universe unification.Pierre-Marie Pédrot
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-10-01Remove spurious uses of CoInductive in SSR prerequisite.Pierre-Marie Pédrot
2019-10-01Fix Print All of section variablesGaëtan Gilbert
2019-10-01Merge PR #10797: Implement discharging in kernelGaëtan Gilbert
2019-09-29Merge PR #10673: [lemmas] Cleanup users of default proof information.Pierre-Marie Pédrot
2019-09-28Remove the monomorphic universe libobject.Pierre-Marie Pédrot
2019-09-26Move the declararation of delayed constraints out of add_constant_aux.Pierre-Marie Pédrot
2019-09-26Implement section discharging inside kernel.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-25Replace custom timeout logic with new GitLab's per-job timeout keyword.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 14:51:45 +0000