aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2018-10-19Merge PR #8758: [api] Qualify access to `Nametab`Hugo Herbelin
2018-10-18[universes] deprecate constr_of_globalMatthieu Sozeau
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-17[micromega] Build csdpcertEmilio Jesus Gallego Arias
2018-10-17Merge PR #8694: Various cleanups of universe apisPierre-Marie Pédrot
2018-10-17Merge PR #8710: [omega, btauto] Remove some dead codePierre-Marie Pédrot
2018-10-17[dune] [plugins] Fix plugin name ground -> firstorderEmilio Jesus Gallego Arias
2018-10-16Merge PR #8738: [clib] Deprecate string functions available in OCaml 4.05Pierre-Marie Pédrot
2018-10-16{Univops->UState}.restrict_universe_contextGaëtan Gilbert
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-16Deprecate univ-dropping UnivGen.new_sort_in_familyGaëtan Gilbert
2018-10-16Remove [constr_of_global_in_context] in funindGaëtan Gilbert
2018-10-16[Omega] Remove dead codeVincent Laporte
2018-10-16[btauto] Remove dead codeVincent Laporte
2018-10-16[omega] Remove dead codeVincent Laporte
2018-10-16[clib] Deprecate string functions available in OCaml 4.05Emilio Jesus Gallego Arias
2018-10-16[micromega] remove dead codeVincent Laporte
2018-10-16[nsatz] remove dead codeVincent Laporte
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Providing a centralized API for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-10-11Merge PR #8699: [quote] Remove spurious file after deletion of quote plugin.Théo Zimmermann
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-11Merge PR #8161: Implement VERNAC EXTEND in coqppMaxime Dénès
2018-10-10[quote] Remove spurious file after deletion of quote plugin.Emilio Jesus Gallego Arias
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
2018-10-08Merge PR #8668: Missing headers in two filesThéo Zimmermann
2018-10-08Merge PR #8554: Fixes #8553: regression of tactic "change" under binders.Pierre-Marie Pédrot
2018-10-07Adding missing header in functional_principles_types.ml.Hugo Herbelin
2018-10-07[api] Deprecate `evar_map` ref combinators.Emilio Jesus Gallego Arias
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-04Merge PR #8626: [ocaml] [lib] Remove some compatibility layers for OCaml < 4....Pierre-Marie Pédrot
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-10-02[ocaml] [lib] Remove some compatibility layers for OCaml < 4.03.0Emilio Jesus Gallego Arias
2018-10-02Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.Pierre-Marie Pédrot
2018-10-02Port g_derive to coqpp.Pierre-Marie Pédrot
2018-10-02Pass unnamed arguments to ML macros.Pierre-Marie Pédrot
2018-09-27Merge PR #8570: [ssr] [camlp5] Remove warning from camlp5Enrico Tassi
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
2018-09-27[ssr] [camlp5] Remove warning from camlp5Emilio Jesus Gallego Arias
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-26Merge PR #8506: [ssr] use the right environment in ssrpattern (fix #8454)Maxime Dénès
2018-09-26Merge PR #8534: Checking if low-level name printers are used on purpose or notMaxime Dénès
2018-09-25Remove romegaVincent Laporte
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:26:59 +0000