aboutsummaryrefslogtreecommitdiff
path: root/CHANGES.md
AgeCommit message (Expand)Author
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-11Fix #9508: Unexpected interaction between implicit arguments and primitive pr...Pierre-Marie Pédrot
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
2019-02-05Add an option not to register Ltac backtraces.Pierre-Marie Pédrot
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Enrich implicits for instancesJasper Hugunin
2019-02-04Primitive integersMaxime Dénès
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
2019-01-25Added a line about notation bug fixes.Hugo Herbelin
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...Jason Gross
2019-01-24Update CHANGESJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-22Update CHANGES.mdEnrico
2019-01-22Apply suggestions from code reviewThéo Zimmermann
2019-01-21[ssr] better structure the ipats docEnrico Tassi
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 09:42:48 +0000