aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-08-16Merge PR #951: Makefile: install-byte works even if -coqide noMaxime Dénès
2017-08-16Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsMaxime Dénès
2017-08-16Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)Maxime Dénès
2017-08-16Merge PR #944: Fix typos. Improve wording.Maxime Dénès
2017-08-16Merge PR #943: Reference Manual: minor wording improvementsMaxime Dénès
2017-08-16Merge PR #940: Replace jarring use of "Remark" with "Note"Maxime Dénès
2017-08-16Merge PR #934: Fix some coq-tex errors in the reference manual.Maxime Dénès
2017-08-16Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wr...Maxime Dénès
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-08-12Merge PR #963: fix coq_makefileMaxime Dénès
2017-08-12fix coq_makefileMatej Košík
2017-08-04Makefile: install-byte works even if -coqide noEnrico Tassi
2017-08-03Amend wording to capture intended meaningSam Pablo Kuper
2017-08-02Update Setoid.texlarsr
2017-08-02Makefile: 'make clean' now immune to the check for binary files without sourcesPierre Letouzey
2017-08-02Typo in the documentation of cumulativityAmin Timany
2017-08-01Fix typos. Improve wording.Sam Pablo Kuper
2017-08-01Improve style slightlySam Pablo Kuper
2017-08-01Merge PR #933: Fix documentation of Hint Mode (bug #4911).Maxime Dénès
2017-08-01Merge PR #932: Fix shuffled documentation.Maxime Dénès
2017-08-01Merge PR #929: Add missing paragraph to introductionMaxime Dénès
2017-08-01Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Maxime Dénès
2017-08-01Merge PR #926: test-suite uses Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #925: Document Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #921: [make] remove compat5 file.Maxime Dénès
2017-08-01Merge PR #919: Remove a few useless evar-normalizations in printing code.Maxime Dénès
2017-08-01Merge PR #917: Moving --print-version to -print-version for consistency.Maxime Dénès
2017-08-01Merge PR #913: Less allocations in DetypingMaxime Dénès
2017-08-01Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Maxime Dénès
2017-08-01Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.Maxime Dénès
2017-08-01Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Maxime Dénès
2017-08-01Merge PR #806: closing bug 5315Maxime Dénès
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-07-31Fix incorrect use of "At the end".Sam Pablo Kuper
2017-07-31Minor grammar fix: replace a "then" with a "so".Sam Pablo Kuper
2017-07-31Replace jarring use of "Remark" with "Note"Sam Pablo Kuper
2017-07-31Update documentation of cumulativityAmin Timany
2017-07-31Improve errors for cumulativity when monomorphicAmin Timany
2017-07-31Change the option for cumulativityAmin Timany
2017-07-31Fix typo and Add Jason's example to the docAmin Timany
2017-07-31Improve documentation of cumulativityAmin Timany
2017-07-31Add Jason's example of fun-ext with cumulativityAmin Timany
2017-07-31Add test for NonCumulative inductivesAmin Timany
2017-07-31Issue error on monomorphic cumulative inductivesAmin Timany
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-31Merge PR #746: Timing on ci via coq_makefile for various projectsMaxime Dénès
2017-07-29Drop paragraph mentioning Addendum as separate doc.Théo Zimmermann
2017-07-29closing bug 5315Julien Forest
2017-07-28Merge PR #923: [api] Fix base_include LTAC parts.Maxime Dénès
2017-07-28Merge PR #889: Removing template polymorphism for definitions.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-23 06:31:27 +0000