aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-01-29Merge PR #9421: [vernac] Fix classification of `Declare Custom Entry`Enrico Tassi
2019-01-29Merge PR #9383: Remove travisVincent Laporte
2019-01-29Merge PR #9424: Surround "assumption" with :tacn:`` in tactics.rstThéo Zimmermann
2019-01-29[test-suite] Fix display of check.Emilio Jesus Gallego Arias
2019-01-28Make lazy_match! goal actually lazyJason Gross
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[vernac] Fix classification of `Declare Custom Entry`Emilio Jesus Gallego Arias
2019-01-28[doc] Remove emacs mentions from INSTALLEmilio Jesus Gallego Arias
2019-01-28Merge pull request coq/ltac2#94 from maximedenes/proof-modePierre-Marie Pédrot
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-26Simplify the GitHub issue templateTej Chajed
2019-01-25Move non-primitive-record warning to declare_mutual_inductive_with_eliminationsGaëtan Gilbert
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-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2019-01-24Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].Hugo Herbelin
2019-01-24Add some quot/rem test-cases for niaJason Gross
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-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
2019-01-24Add subst to the end of nia in the test-suiteJason Gross
2019-01-24Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanupJason Gross
2019-01-24Remove remainder of `Abort`s in test-suite Nia.vJason Gross
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
2019-01-24Don't pose any disjunctions in div_mod_to_quot_remJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
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-24Make `Instance` without a body always open a proof.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 07:35:12 +0000