aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-01-29Merge PR #9383: Remove travisVincent Laporte
2019-01-29Merge PR #9424: Surround "assumption" with :tacn:`` in tactics.rstThéo Zimmermann
2019-01-28Surround "assumption" with :tacn:`` in tactics.rstRyan Scott
2019-01-28Merge PR #9420: [doc] Remove emacs mentions from INSTALLThéo Zimmermann
2019-01-28[doc] Remove emacs mentions from INSTALLEmilio Jesus Gallego Arias
2019-01-28Merge PR #9402: Move \def\plus and \def\tri to refman-preamble.sty.Théo Zimmermann
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
2019-01-27Merge PR #9399: [ide] fail on unavailable commands before adding to the documentEmilio Jesus Gallego Arias
2019-01-27[test] for bug #9385Enrico Tassi
2019-01-27[fake_ide] infrastructure to test the failure of an ADDEnrico Tassi
2019-01-27[ide] fail on unavailable commands before adding to the documentEnrico Tassi
2019-01-27Merge PR #9263: [STM] explicit handling of parsing statesEmilio Jesus Gallego Arias
2019-01-27Merge PR #9214: Notations: Removing useless parentheses on abbreviations shor...Emilio Jesus Gallego Arias
2019-01-25Merge PR #9362: Fix makefile .merlin for unit testsEnrico Tassi
2019-01-25Merge PR #9391: Clarify meaning of Primitive ProjectionsThéo Zimmermann
2019-01-25Merge PR #8637: Update -compat to support -compat 8.10Théo Zimmermann
2019-01-25Added a line about notation bug fixes.Hugo Herbelin
2019-01-25Notations: Removing useless parentheses on abbrevs for prefix of an application.Hugo Herbelin
2019-01-24Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].Hugo Herbelin
2019-01-24Update update-compat.py and release-process.mdJason Gross
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-24Update update-compat.py scriptJason Gross
2019-01-25Move \def\plus and \def\tri to refman-preamble.sty.Tanaka Akira
2019-01-24Merge PR #9384: Improve the note in the beginning of the Ltac chapter.Clément Pit-Claudel
2019-01-24Add OverlaysMaxime Dénès
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2019-01-24[STM] API to print a Stateid.tEnrico Tassi
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
2019-01-24Merge PR #9392: Fix small errors in cic.rst.Théo Zimmermann
2019-01-24Merge PR #9394: [nix-ci] MaintenanceThéo Zimmermann
2019-01-24[nix-CI] Split the build inputsVincent Laporte
2019-01-24[Nix-ci] Add QuickChickVincent Laporte
2019-01-24[Nix-ci] Fix UnicoqVincent Laporte
2019-01-24[Nix-ci] Add formal-topologyVincent Laporte
2019-01-24Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)Matthieu Sozeau
2019-01-24[doc] warn that (automatic) clears can result in errorsEnrico Tassi
2019-01-24[doc] more precise description of when automatic clears are triggeredEnrico Tassi
2019-01-24[doc] explain how to avoid automatic clearsEnrico Tassi
2019-01-24Merge PR #9372: [thread] protect threads against sigalrmEmilio Jesus Gallego Arias
2019-01-24add commentEnrico Tassi
2019-01-24use \nO, \nS, etc. fix \kw{n}.Tanaka Akira
2019-01-24Fix small errors in cic.rst.Tanaka Akira
2019-01-23Clarify meaning of Primitive ProjectionsDavid A. Dalrymple
2019-01-23Move and rewrite documentation for intro patterns that was underJim Fehrle
2019-01-23Merge PR #9357: Fix recursive loadpath of ML filesEmilio Jesus Gallego Arias
2019-01-23Merge PR #9043: [windows] Cleanup cruft from `dev/build/windows`Michael Soegtrop
2019-01-23Merge PR #9270: Turn `Refine instance Mode` off by defaultPierre-Marie Pédrot
2019-01-23Merge PR #9374: Documentation: ring and field simplify can take no argumentsThéo Zimmermann
2019-01-23Fix the information of the level of ; vs ; [ ]Théo Zimmermann
2019-01-23Merge PR #9347: At Qed, if shelved goals remain, emit a warning instead of an...Pierre-Marie Pédrot