aboutsummaryrefslogtreecommitdiff
path: root/CHANGES.md
AgeCommit message (Expand)Author
2018-12-20Merge PR #8488: Warning when using automatic template polymorphismPierre-Marie Pédrot
2018-12-19Add CHANGES for auto-template warning.Gaëtan Gilbert
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-12Accept argument names for extra arguments with "extra scopes"Maxime Dénès
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-10Merge PR #7221: The usual order of strings.Hugo Herbelin
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-23Doc for Private Polymorphic Universes.Gaëtan Gilbert
2018-11-22The usual order of strings.Yao Li
2018-11-22Deprecate Typeclasses Axioms Are InstancesGaëtan Gilbert
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-19Merge PR #8987: Deprecate hint declaration/removal with no specified databasePierre-Marie Pédrot
2018-11-19Merge PR #9001: [options] Remove deprecated option automatic introduction.Pierre-Marie Pédrot
2018-11-19Merge PR #9013: Do not Export the init modulesPierre-Marie Pédrot
2018-11-19Merge PR #8451: Print Universes SubgraphPierre-Marie Pédrot
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-16Print Universes SubgraphGaëtan Gilbert
2018-11-16Do not Export the init modulesGaëtan Gilbert
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-15coqide: use correct toplevel name in filesGaëtan Gilbert
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-11-11Merge PR #8795: Encapsulating declarations of primitive string syntax in a mo...Jason Gross
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
2018-11-06Move features that were not backported to 8.9 to the 8.10 section of CHANGES.md.Théo Zimmermann
2018-11-05Merge PR #8815: NArith: add lemmas about numbers and vectorsHugo Herbelin
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-10-29NArith: implicit length argument for Bv2NYishuai Li
2018-10-29NArith: add lemmas about numbers and vectorsYishuai Li
2018-10-23Encapsulating declarations of primitive string syntax in a module.Hugo Herbelin
2018-10-17Strings: add ByteVectorYishuai Li
2018-10-10Add minimal CHANGES entry about compat notationsJason Gross
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
2018-10-06Merge PR #8555: Remove section paths from kernel namesPierre-Marie Pédrot
2018-10-05Rename CHANGES to CHANGES.md.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:11:58 +0000