aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR #6759: detype_case predicate is not optionalGravatar Maxime Dénès2018-02-19
|\
* \ Merge PR #6772: Cleanup inferCumulativityGravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6648: [tactics] make apply_type safeGravatar Maxime Dénès2018-02-19
|\ \ \
* \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Gravatar Maxime Dénès2018-02-19
|\ \ \ \
* \ \ \ \ Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6571: Fix ci-all targetGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \
| | | | * | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | * | | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| |_|_|_|/ / / |/| | | | | |
| | | | | * | Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| | | | | * | Fix reduction flags in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| |_|_|_|/ / |/| | | | |
* | | | | | Merge PR #1073: new quick2vo target: like vio2vo, but smarterGravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \
| * | | | | | disable tests: vio2vo is broken in WindowsGravatar Ralf Jung2018-02-15
| * | | | | | also test vio2voGravatar Ralf Jung2018-02-15
| * | | | | | test "make quick2vo"Gravatar Ralf Jung2018-02-15
| * | | | | | new quick2vo target: like vio2vo, but smarterGravatar Ralf Jung2018-02-15
| | |_|_|/ / | |/| | | |
* | | | | | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectGravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \
| * | | | | | coq_makefile: Support "" as the prefix in _CoqProjectGravatar Joachim Breitner2018-02-15
* | | | | | | Merge PR #6760: CHANGES for 8.7.2.Gravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \ \
| * | | | | | | CHANGES for 8.7.2.Gravatar Théo Zimmermann2018-02-14
|/ / / / / / /
| | | | | | * detype_case predicate is not optionalGravatar Gaëtan Gilbert2018-02-14
* | | | | | | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Gravatar Maxime Dénès2018-02-14
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\ \ \ \ \ \ \ \
| | | | | | * | | [build] Fix VM dynamic linking prep in byte builds.Gravatar Emilio Jesus Gallego Arias2018-02-14
| | | | |_|/ / / | | | |/| | | |
| | | | | | * | coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGravatar Gaëtan Gilbert2018-02-13
| | * | | | | | Add CHANGES entry for #1047Gravatar Tej Chajed2018-02-13
| | |/ / / / /
| | | | | * | coqdev.el: fix "compilate"-command typoGravatar Gaëtan Gilbert2018-02-13
| | | | | * | coqdev.el: shell-quote-argument the directory for make -CGravatar Gaëtan Gilbert2018-02-13
| | | | | * | coqdev.el: stop using when-let for emacs<25 compatibility.Gravatar Gaëtan Gilbert2018-02-13
* | | | | | | Merge PR #6693: [toplevel] Refactor command line argument handling.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking l...Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ |/| | | | | | | | |
* | | | | | | | | | Merge PR #6738: CHANGES for universe varianceGravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6565: [Backport script] Check .mli files are not changed.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | * | | | | | | | | CHANGES for universe varianceGravatar Gaëtan Gilbert2018-02-12
| | | | | | | | * | | | Add test case for #6677.Gravatar Maxime Dénès2018-02-12
* | | | | | | | | | | | Merge PR #6262: [error] Replace msg_error by a proper exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6128: Simplification: cumulativity information is variance informa...Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6418: More detailed error messages for Canonical Structure, #6398Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6139: Make list functions returning sumbools transparentGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6718: Fix redirection to stderr in lint-repository error message.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6708: Mention -quiet flag for FailGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6706: ci-common: guess CI_BRANCH for local buildsGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6674: Delay computation of lifts in the reduction machine.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | * | | Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-12
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 14:16:47 +0000