aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-27Merge PR #11199: Correcting unintended changelog message for #11090 (coercion...Théo Zimmermann
2019-11-27Changelog entry for #11187.Théo Zimmermann
2019-11-27Remove deprecated commands `AddPath`, `AddRecPath` and `DelPath`Maxime Dénès
2019-11-27Correcting unintended changelog message for #11090 (coercion+notation regress...Hugo Herbelin
2019-11-27Merge PR #11158: [release] Update files for 8.12 release per release process.Théo Zimmermann
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-27Merge PR #11196: missing " in CONTRIBUTING.mdThéo Zimmermann
2019-11-27missing "Olivier Laurent
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ...Pierre-Marie Pédrot
2019-11-27Merge PR #11193: weaker then -> weaker thanThéo Zimmermann
2019-11-27weaker then -> weaker thanlarsr
2019-11-26Merge PR #11177: Add a complexity test for `pattern`Hugo Herbelin
2019-11-26Merge PR #11179: Fix Windows 32 bit buildEmilio Jesus Gallego Arias
2019-11-26Update test-suite/complexity/pattern.vJason Gross
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-26Merge PR #11180: Add more development setup instructions for tutorialsEmilio Jesus Gallego Arias
2019-11-26Merge PR #11166: Add test for #11161Emilio Jesus Gallego Arias
2019-11-26Fix Windows 32 bit buildPierre Roux
2019-11-26indTyping: error instead of anomaly for ill-formed templateGaëtan Gilbert
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-26Merge PR #11173: [ssr] fix «W -- weakening» docEnrico Tassi
2019-11-26Merge PR #11034: Update update-compat.pyThéo Zimmermann
2019-11-25Add more development setup instructions for tutorialsTalia Ringer
2019-11-25Error fatally if update-compat.py gets no flagJason Gross
2019-11-25Merge PR #11159: Minor fix in doc for [unfold]Théo Zimmermann
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
2019-11-25Add a complexity test for `pattern`Jason Gross
2019-11-24Merge PR #11152: Cache the relevance flag in rel contexts in an efficient way.Gaëtan Gilbert
2019-11-24fix «W -- weakening» docAntonio Nikishaev
2019-11-22Add test for #11161Gaëtan Gilbert
2019-11-22Merge PR #11136: Adding `inj_compr` lemma in ssrfun.Enrico Tassi
2019-11-22Use the relevance flag in CClosure rel contexts in an efficient way.Pierre-Marie Pédrot
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-21Merge PR #11154: add tlc to ci; please proof read very carefully and test. th...Emilio Jesus Gallego Arias
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 #11109: Register proof_irrelevanceEmilio Jesus Gallego Arias
2019-11-21Merge PR #10587: [coqdoc] Nest <a> into <h2> instead of the other way aroundEmilio Jesus Gallego Arias
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
2019-11-21Merge PR #11010: [coq] Untabify the whole ML codebase.Gaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-21add tlc to ci; please proof read very carefully and test. thankscharguer
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 #11103: Grammars: unification fix/cofix between constr/vernac + clea...Emilio Jesus Gallego Arias