aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fixing the printing of unknown locations by adding a newline.Gravatar Pierre-Marie Pédrot2016-07-08
* Adding a breaking space in warning names.Gravatar Pierre-Marie Pédrot2016-07-08
* Remove spurious warnings about projections when requiring modules.Gravatar Pierre-Marie Pédrot2016-07-08
* Fixing #4906 (regression in printing an error message).Gravatar Hugo Herbelin2016-07-08
* Typo in a comment of stdlib.Gravatar Hugo Herbelin2016-07-08
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\
* \ Merge remote-tracking branch 'github/bug4653' into v8.6Gravatar Matthieu Sozeau2016-07-07
|\ \
| | * Prevent "Load" from displaying all the intermediate subgoals.Gravatar Guillaume Melquiond2016-07-07
| | * Do not display goals in -compile-verbose mode (bug #4841).Gravatar Guillaume Melquiond2016-07-07
| * | Do not use implicit type info for (x := t) bindingsGravatar Matthieu Sozeau2016-07-07
* | | Merge remote-tracking branch 'github/bug4873' into v8.6Gravatar Matthieu Sozeau2016-07-07
|\ \ \
| * | | Program: fix #4873: transparency option not usedGravatar Matthieu Sozeau2016-07-07
|/ / /
| | * Update csdp.cache.Gravatar Maxime Dénès2016-07-06
| | * Fix typo in configure (noticed by Jason).Gravatar Maxime Dénès2016-07-06
* | | Merge branch 'primproj' into v8.6Gravatar Matthieu Sozeau2016-07-06
|\ \ \
| * | | Fix reopened bug #3317.Gravatar Matthieu Sozeau2016-07-06
| * | | Fixed bug #4622.Gravatar Matthieu Sozeau2016-07-06
| * | | Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
| * | | Renaming to more generic has_dependent_elim testGravatar Matthieu Sozeau2016-07-06
| * | | Move is_prim... to Inductiveops and correct SchemeGravatar Matthieu Sozeau2016-07-06
| * | | primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
|/ / /
| | * Merge remote-tracking branch 'github/pr/199' into v8.5Gravatar Maxime Dénès2016-07-06
| | |\
| | * \ Merge remote-tracking branch 'github/pr/241' into v8.5Gravatar Maxime Dénès2016-07-06
| | |\ \
* | | | | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| | * | | Bump version number in preparation for 8.5pl2 release.Gravatar Maxime Dénès2016-07-06
| * | | | Fix test-suite file 3690Gravatar Matthieu Sozeau2016-07-06
| | * | | Deduplicate some names in .mailmapGravatar Jason Gross2016-07-06
| * | | | Univs: fix internalization of (x := T) and castsGravatar Matthieu Sozeau2016-07-06
|/ / / /
| * | | Fix indentation of configure printoutGravatar Jason Gross2016-07-06
| | * | Move option_map notation upGravatar Jason Gross2016-07-05
| | * | Restore option_map in FMapFactsGravatar Jason Gross2016-07-05
| |/ /
| | * Compat84: Don't mess with stdlib modulesGravatar Jason Gross2016-07-05
| * | Prevent unsafe overwriting of Required modules by toplevel library.Gravatar Maxime Dénès2016-07-05
| * | congruence fix: test-suite code and update CHANGESGravatar Matthieu Sozeau2016-07-05
* | | Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Gravatar Maxime Dénès2016-07-05
| * | Pass .v files to coqc in Makefile produced by coq_makefile (bug #4896).Gravatar Guillaume Melquiond2016-07-05
| * | Add mailmap entry.Gravatar Guillaume Melquiond2016-07-05
| * | Bug fix : variable capture in ltac code of NsatzGravatar thery2016-07-05
* | | FIX: "dev/doc/changes.txt"Gravatar Matej Kosik2016-07-05
* | | Merge remote-tracking branch 'github/pr/229' into trunkGravatar Maxime Dénès2016-07-04
|\ \ \
| | * \ Merge branch 'congruencefix' into v8.5Gravatar Matthieu Sozeau2016-07-04
| | |\ \
* | | | | Revert "Revert "Improve the interpretation scope of arguments of an ltac matc...Gravatar Maxime Dénès2016-07-04
* | | | | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\ \ \ \ \ | | |/ / / | |/| | |
| | | * | congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
| | | * | congruence: remove casts of indexed termsGravatar Matthieu Sozeau2016-07-04
| | | * | congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
* | | | | Update CHANGES, the bugfixes for 4527 and 4726 areGravatar Matthieu Sozeau2016-07-04
| * | | | Mention more fixes in CHANGES before we release pl2.Gravatar Maxime Dénès2016-07-04
| * | | | Revert "Improve the interpretation scope of arguments of an ltac match."Gravatar Maxime Dénès2016-07-04
| | |/ / | |/| |
| * | | test-suite: test checking of libraries checksum.Gravatar Maxime Dénès2016-07-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 02:43:50 +0000