aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-03-08Merge PR #11740: Ltac2: Add notation for enough and eenoughPierre-Marie Pédrot
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-05Merge PR #11602: Adding support for an "only parsing" modifier in "where"-bas...Pierre-Marie Pédrot
2020-03-04Merge PR #11429: [zify] several efficiency enhancementsVincent Laporte
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-03-03[zify] efficiency improvementsFrédéric Besson
2020-03-03Ltac2: Add notation for enough and eenoughMichael Soegtrop
2020-03-03Update doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rstHugo Herbelin
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
2020-02-28Deprecating the declaration of arbitrary terms as hints.Pierre-Marie Pédrot
2020-02-28Adding change logHugo Herbelin
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-26Fix changelog for https://github.com/coq/coq/pull/11686Maxime Dénès
2020-02-26Consolidate int63-related notationsMaxime Dénès
2020-02-25Merge PR #11663: Remove unqualified universe attributes.Emilio Jesus Gallego Arias
2020-02-24added changelogAbhishek Anand (optiplex7010@home)
2020-02-23Remove unqualified universe attributes.Théo Zimmermann
2020-02-23Addressing a changelog comment from Théo Zimmermann.Hugo Herbelin
2020-02-23Update doc/changelog/03-notations/11120-master+refactoring-application-printi...Hugo Herbelin
2020-02-23Apply and generalize suggestions from Théo.Hugo Herbelin
2020-02-22Adding a changelog item.Hugo Herbelin
2020-02-21Merge PR #11590: Fixes #9741: only printing notations do not uselessly reserv...Emilio Jesus Gallego Arias
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
2020-02-21Adding changelog for #11590, fixing #9741.Hugo Herbelin
2020-02-21Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.Gaëtan Gilbert
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...Emilio Jesus Gallego Arias
2020-02-20[init] Add `-boot` option to avoid binding `Coq.` prefix.Emilio Jesus Gallego Arias
2020-02-21Merge PR #11329: Fixing #11114: anomaly with Extraction Implicit on records.Kazuhiko Sakaguchi
2020-02-20Merge PR #11616: [coqdep] Tweak changelog after recent PRs.Gaëtan Gilbert
2020-02-20Adding changelog.Hugo Herbelin
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
2020-02-19Adding change log for #10832.Hugo Herbelin
2020-02-18Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)Pierre-Marie Pédrot
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
2020-02-17[coqdep] Tweak changelog after recent PRs.Emilio Jesus Gallego Arias
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-16Adding change log.Hugo Herbelin
2020-02-13Merge PR #11441: Add explicit types to changelog entries that were still miss...Emilio Jesus Gallego Arias
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
2020-02-11Lately adding a changelog for PR#10202.Hugo Herbelin
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
2020-02-08Merge PR #10343: Resolve 10342 : [Ltac2] Add array libraryPierre-Marie Pédrot
2020-02-08Merge PR #11404: replace RList by list R in all files where it is used in thi...Pierre-Marie Pédrot
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-02-07[coqdep] Add changelog for recent modifications.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 17:10:02 +0000