aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-01-31Remove "End TreeExample." line.Tanaka Akira
2019-01-31Merge PR #8720: [Numeral notations] Use Coqlib registered constantsEmilio Jesus Gallego Arias
2019-01-30Update Cachix signing key.Théo Zimmermann
2019-01-30Updated pinned nixpkgs.Théo Zimmermann
2019-01-30Merge PR #9440: Create deployment environment for Cachix.Emilio Jesus Gallego Arias
2019-01-30Create deployment environment for Cachix.Théo Zimmermann
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-30Cleanup universe length for inductives in vconvGaëtan Gilbert
2019-01-30Restrict universes in records.Gaëtan Gilbert
2019-01-30Comment universe operations in Classes.contextGaëtan Gilbert
2019-01-30Merge pull request coq/ltac2#100 from JasonGross/fix-lazy-match-goalPierre-Marie Pédrot
2019-01-29Merge PR #9417: Update update-compat.py scriptThéo Zimmermann
2019-01-29Merge PR #9435: Use \mathcal instead of \calThéo Zimmermann
2019-01-29Update update-compat.py scriptJason Gross
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
2019-01-29[test-suite] Display full paths on CHECK.Emilio Jesus Gallego Arias
2019-01-29Use \mathcal instead of \calGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 07:03:36 +0000