Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #864: Some cleanups after cumulativity for inductive types | 2017-08-16 | |
|\ | |||
* \ | Merge PR #963: fix coq_makefile | 2017-08-12 | |
|\ \ | |||
| * | | fix coq_makefile | 2017-08-12 | |
|/ / | |||
* | | Makefile: 'make clean' now immune to the check for binary files without sources | 2017-08-02 | |
| * | Typo in the documentation of cumulativity | 2017-08-02 | |
* | | Merge PR #933: Fix documentation of Hint Mode (bug #4911). | 2017-08-01 | |
|\ \ | |||
* \ \ | Merge PR #932: Fix shuffled documentation. | 2017-08-01 | |
|\ \ \ | |||
* \ \ \ | Merge PR #929: Add missing paragraph to introduction | 2017-08-01 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas). | 2017-08-01 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #926: test-suite uses Extraction TestCompile | 2017-08-01 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #925: Document Extraction TestCompile | 2017-08-01 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #921: [make] remove compat5 file. | 2017-08-01 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #919: Remove a few useless evar-normalizations in printing code. | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #917: Moving --print-version to -print-version for consistency. | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #913: Less allocations in Detyping | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709) | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND. | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #834: Adding support for recursive notations of the form "x , .. , y... | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #806: closing bug 5315 | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | 2017-08-01 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | | * | Update documentation of cumulativity | 2017-07-31 | |
| | | | | | | | | | | | | | | | * | Improve errors for cumulativity when monomorphic | 2017-07-31 | |
| | | | | | | | | | | | | | | | * | Change the option for cumulativity | 2017-07-31 | |
| | | | | | | | | | | | | | | | * | Fix typo and Add Jason's example to the doc | 2017-07-31 | |
| | | | | | | | | | | | | | | | * | Improve documentation of cumulativity | 2017-07-31 | |
| | | | | | | | | | | | | | | | * | Add Jason's example of fun-ext with cumulativity | 2017-07-31 | |
| | | | | | | | | | | | | | | | * | Add test for NonCumulative inductives | 2017-07-31 | |
| | | | | | | | | | | | | | | | * | Issue error on monomorphic cumulative inductives | 2017-07-31 | |
* | | | | | | | | | | | | | | | | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | 2017-07-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #746: Timing on ci via coq_makefile for various projects | 2017-07-31 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | * | | | Drop paragraph mentioning Addendum as separate doc. | 2017-07-29 | |
| | | | * | | | | | | | | | | | | | | closing bug 5315 | 2017-07-29 | |
| |_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | | | | Merge PR #923: [api] Fix base_include LTAC parts. | 2017-07-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #889: Removing template polymorphism for definitions. | 2017-07-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #888: Stronger kernel types | 2017-07-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #823: Async off in Windows by default in CoqIDE | 2017-07-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #782: Update API for fiat | 2017-07-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | | | | | | | * | Fix documentation of Hint Mode (bug #4911). | 2017-07-28 | |
| | | | | | | | | | | | | | | | | | | | * | | Fix shuffled documentation. | 2017-07-28 | |
| | | | | | | | | | | | | | | | | | | | |/ | |||
* | | | | | | | | | | | | | | | | | | | | | Merge PR #852: Makefile: fails if some .vo or .cm* file has no source | 2017-07-28 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | | | | | | * | | Add missing paragraph to introduction | 2017-07-27 | |
| | | | | | | | | | | | | | | | | | | | |/ | |||
| | | | | | | | | | | | | | | | | | | * / | Fixing bug #5671 (specialize unclean wrt Metas). | 2017-07-27 | |
| | | | | | | | | | | | | | | | | | | |/ | |||
| | | | | | | | | | | | | | | | | * | | | Extraction.tex: mention the possible "From Coq Require Extraction" | 2017-07-27 | |
| | | | | | | | | | | | | | | | | * | | | Extraction TestCompile documented + mentionned in CHANGES | 2017-07-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | * | | test-suite: more use of the new command Extraction TestCompile | 2017-07-27 | |
| | | | | | | | | * | | | | | | | | | | [toplevel] Remove long ago deprecated and NOOP options. | 2017-07-27 | |
| | | | | | | | | | |_|_|_|_|_|_|_|/ | | | | | | | | | |/| | | | | | | | | |||
| | | | | | | | | | | | | | | | * | | [make] remove compat5 file. | 2017-07-27 | |
| | | | | | | | | | |_|_|_|_|_|/ / | | | | | | | | | |/| | | | | | | | |||
| | | | | | * | | / | | | | | | | | [api] Fix base_include LTAC parts. | 2017-07-27 | |
| | | | | | | |_|/ / / / / / / / | | | | | | |/| | | | | | | | | | |||
| | | | | | | | * | | | | | | | | deprecate Pp.std_ppcmds type alias | 2017-07-27 | |
| | | | | | * | | | | | | | | | | Fix TypeclassDebug.out after conflicting PR merges | 2017-07-26 | |
| |_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | |