aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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-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
2018-09-24Merge PR #8499: [api] Deprecate constructors of deprecated datatypes.Pierre-Marie Pédrot
2018-09-24Merge PR #8464: Fix numeral notationsHugo Herbelin
2018-09-23[api] Deprecate constructors of deprecated datatypes.Emilio Jesus Gallego Arias
2018-09-23Merge PR #8465: Small cleanup of summary usesPierre-Marie Pédrot
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-21Merge pull request #8462 from vbgl/zify-colonequalLaurent Théry
2018-09-20Merge PR #8297: Fix #7754: universe declarations on mutual inductivesMatthieu Sozeau
2018-09-19Fix Numeral Notations (4/4 - fixing synch)Jason Gross
2018-09-19Fix Numeral Notations (3/4 - moving more stuff)Jason Gross
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
2018-09-19Fix Numeral Notations (1/4 - moving things)Jason Gross
2018-09-19Merge PR #8246: Implementing an internal basic version of the "pose" tactic i...Enrico Tassi
2018-09-19[ssr] use the right environment in ssrpattern (fix #8454)Enrico Tassi
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-19Remove Hints.add_hints_initGaëtan Gilbert
2018-09-19Merge PR #8447: Cleaning in the retroknowledgePierre-Marie Pédrot
2018-09-18Zify: replace local definitions by equationsVincent Laporte
2018-09-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: simpler parsing rulesVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-13Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernelMaxime Dénès
2018-09-13Add explicit atribute for template polymorphism.Gaëtan Gilbert
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-09-12Remove quote pluginMaxime Dénès
2018-09-11Merge PR #7288: Isolating ltac naming out of pretyping + fixing renamingPierre-Marie Pédrot
2018-09-11Merge PR #8284: [ssr] anomaly -> errorMaxime Dénès
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-09-10Deprecate romega in favor of lia.Vincent Laporte