aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-11-30Deprecation annotation for `convert_concl_no_check`Maxime Dénès
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-29Merge PR #10931: Add types of changes to changelog entries.Emilio Jesus Gallego Arias
2019-11-28Release notes for Coq 8.10.2Vincent Laporte
2019-11-28Update README and make-changelog tool following introduction of changelog types.Théo Zimmermann
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
2019-11-28Fix extension of changelog file.Théo Zimmermann
2019-11-27Merge PR #11187: Remove deprecated commands `AddPath`, `AddRecPath` and `DelP...Emilio Jesus Gallego Arias
2019-11-27Changelog entry for #11187.Théo Zimmermann
2019-11-27Correcting unintended changelog message for #11090 (coercion+notation regress...Hugo Herbelin
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-27weaker then -> weaker thanlarsr
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
2019-11-26Make rapply handle all numbers of underscoresJason Gross
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-25Add more development setup instructions for tutorialsTalia Ringer
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
2019-11-22Merge PR #11136: Adding `inj_compr` lemma in ssrfun.Enrico Tassi
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-21Merge PR #11145: Document -vos flag for coqdepEmilio Jesus Gallego Arias
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fi...Emilio Jesus Gallego Arias
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
2019-11-21Document -vos flag for coqdepGaëtan Gilbert
2019-11-21Update doc/changelog/02-specification-language/11132-master+fix-implicit-let-...Hugo Herbelin
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-21Taking @Zimmi48's comment into accountCyril Cohen
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-19coq_makefile: support COQBIN with no ending /Gaëtan Gilbert
2019-11-19added changelog entryCyril Cohen
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-15Update doc/changelog/04-tactics/10998-zify-complements.rstKazuhiko Sakaguchi
2019-11-15Add missing zify class instancesKazuhiko Sakaguchi
2019-11-14Merge PR #10979: Fix doc for universes(foo) attributesThéo Zimmermann
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
2019-11-14doc fixesAntonio Nikishaev
2019-11-14Restore documentation of `Typeclasses Axioms Are Instances`Maxime Dénès
2019-11-14Document recommended syntax for `firstorder`Maxime Dénès
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-04Cite POPL19 SProp paperGaëtan Gilbert
2019-11-03Elan → Stratego in documentation of `rewrite_strat`.Robbert Krebbers
2019-11-01Merge PR #11028: Update the deprecation doc of `Shrink Obligations`Clément Pit-Claudel
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01Update the deprecation doc of `Shrink Obligations`Jason Gross