| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | * | | | | | | | | | | | | Update Setoid.tex |  larsr | 2017-08-02 | |
| | |_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | Makefile: 'make clean' now immune to the check for binary files without sources |  Pierre Letouzey | 2017-08-02 | |
| | * | | | | | | | | | | | | | | | | | Typo in the documentation of cumulativity |  Amin Timany | 2017-08-02 | |
| | | | | | | | | | | | | | * | | | | | Unbreak RecTutorial.v |  Gaëtan Gilbert | 2017-08-01 | |
| | | | | | | | | | | | | | * | | | | | Remove old doc/rt files. | Gaëtan Gilbert | 2017-08-01 | |
| | | | | | | | | | | | | | * | | | | | Add dev/v8-syntax/check-grammar byproducts to gitignore. | Gaëtan Gilbert | 2017-08-01 | |
| | | | | | | | | | | | | | * | | | | | Remove obsolete files | Gaëtan Gilbert | 2017-08-01 | |
| | | | | | | | | | | | | | * | | | | | Add .v extension to dev/doc/notes-on-conversion | Gaëtan Gilbert | 2017-08-01 | |
| | | | | | | | | | | | | | * | | | | | Remove dev/TODO | Gaëtan Gilbert | 2017-08-01 | |
| | | | | | | | | | | | | | * | | | | | Fix syntax-v8.tex bad parenthesizing | Gaëtan Gilbert | 2017-08-01 | |
| | | | | | | | | | | | | | * | | | | | Remove unused Makefiles in dev/tools/ | Gaëtan Gilbert | 2017-08-01 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | | | | | [flags] Remove XML output flag. |  Emilio Jesus Gallego Arias | 2017-08-01 | |
| | |_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | * | Remove understand_tcc_evars. |  Maxime Dénès | 2017-08-01 | |
| | | | | | | | | | | | | | | | * | Move type_uconstr to Tacinterp. | Maxime Dénès | 2017-08-01 | |
| | | | | | | | | | | | | | * | | | Have coq-dpdgraph ci test print the differences |  Jason Gross | 2017-08-01 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | Remove understand_judgment and understand_judgment_tcc. | Maxime Dénès | 2017-08-01 | |
| | | | | | | | | | | | | | | * | Remove allow_anonymous_refs. | Maxime Dénès | 2017-08-01 | |
| | | | | | | | | | | | | | | * | Remove pure_open_constr (now open_constr) | Maxime Dénès | 2017-08-01 | |
| | | | | | | | | | * | | | | | | Printing goals does not evar-normalizes beforehand anymore. |  Pierre-Marie Pédrot | 2017-08-01 | |
| | | | | | | | | | * | | | | | | Detyping functions are now operating on EConstr.t. | Pierre-Marie Pédrot | 2017-08-01 | |
| | |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | Fix typos. Improve wording. |  Sam Pablo Kuper | 2017-08-01 | |
| | | | | * | | | | | | | | | | Improve style slightly | Sam Pablo Kuper | 2017-08-01 | |
| | | | | | | | | | | | | | * | Move glob_constr_ltac_closure to evar_refiner. | Maxime Dénès | 2017-08-01 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | Merge PR #933: Fix documentation of Hint Mode (bug #4911). | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #932: Fix shuffled documentation. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #929: Add missing paragraph to introduction | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas). | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #926: test-suite uses Extraction TestCompile | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #925: Document Extraction TestCompile | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #921: [make] remove compat5 file. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #917: Moving --print-version to -print-version for consistency. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #913: Less allocations in Detyping | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709) | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #834: Adding support for recursive notations of the form "x , .. , y... | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #806: closing bug 5315 | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | | | | | | * | | | | | adding a comment to explain the change |  Julien Forest | 2017-08-01 | |
| | | | | | | | | | | | | | | | | | | | | | | | * | | | | | solving b1859 | Julien Forest | 2017-08-01 | |
| | | | | | | | | | | | | | | | | | | | | | | |/ / / / / | | | | | | | | | | | | | | | | | | | | | |/| | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | * | | | | | | | Fix incorrect use of "At the end". | Sam Pablo Kuper | 2017-07-31 | |
| | | | | | | | | | | | | | | | | | | | | * | | | | | | | Minor grammar fix: replace a "then" with a "so". | Sam Pablo Kuper | 2017-07-31 | |
| | | | | | | | | | | | | | | | | | | | | |/ / / / / / | ||||
| | | | | | | | | | | | | | | | | | | | * / / / / / / | Replace jarring use of "Remark" with "Note" | Sam Pablo Kuper | 2017-07-31 | |
| | | | | | | | | | | | | | | | | | | | |/ / / / / / | ||||
| | | | | | | | | | | | | | | | | * | | | | | | | | | Update documentation of cumulativity | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | | Improve errors for cumulativity when monomorphic | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | | Change the option for cumulativity | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | | Fix typo and Add Jason's example to the doc | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | | Improve documentation of cumulativity | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | | Add Jason's example of fun-ext with cumulativity | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | * | | | | | | | | | Add test for NonCumulative inductives | Amin Timany | 2017-07-31 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |