aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* | | | | | | | | | | Merge PR #6738: CHANGES for universe varianceGravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| | | | | | | | |_|_|/ | | | | | | | |/| | |
* | | | | | | | | | | 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
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | inferCumulativity: add comment to explain [if not is_arity].Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | * | | | | | | | | | | Documentation for cumulative inductive variance.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | * | | | | | | | | | | Print inductive cumulativity info in About.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | * | | | | | | | | | | Universe instance printer: add optional variance argument.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | * | | | | | | | | | | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | * Merge anomaly-traces-parser.el into coqdev.el.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | * coqdev.el: add installation instructions.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | * | | | | | | | | | | Inference of inductive subtyping does not need an evar map.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | * | | | | | | | | | | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | * | | | | | | | | | | [get_cumulativity_constraints] allowing further code sharing.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | * | | | | | | | | | | Factorize code for comparing maybe-cumulative inductives.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | * | | | | | | | | | | Fix typo in Univ.CumulativityInfoGravatar Gaëtan Gilbert2018-02-10
| |_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | | | [vernac] Fix outdated comment.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | | | | * | | | [nit] Remove some unnecessary global `open Feedback`Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | | | | * | | | [vernac] [minor] Move print effects to top-level caller.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | |_|_|_|/ / / / | | | | | | | | | | |/| | | | | | |
| | | | | | | | | | * | | | | | | | [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | |/ / / / / / / / | | | | | | | | |/| | | | | | | |
| | | | | | | | * | | | | | | | | [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| |_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | [toplevel] Small refactoring of fatal_error functions.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | | * | | [toplevel] Refactor command line argument handling.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | |/ / /
| | | | | * | | | | | | / / / Fix redirection to stderr in lint-repository error message.Gravatar Gaëtan Gilbert2018-02-08
| |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | |
| | | | * | | | | | | | | | mention interactive mode for Fail messageGravatar Paul Steckler2018-02-07
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | | | | * | | [toplevel] Disable error resiliency in `-quick` mode.Gravatar Emilio Jesus Gallego Arias2018-02-07
| |_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #6657: Document the Fail commandGravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6685: Use whd-all on rigid-flex conversion.Gravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6610: Points to Flocq official repository.Gravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6673: Fix evar handling in native_compute conversionGravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | | | | | ci-common: guess CI_BRANCH for local buildsGravatar Gaëtan Gilbert2018-02-07
| |_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | Possible fix for issue #6697Gravatar Yannick Forster2018-02-07
| |_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | |
| | | | | | | | | * | | | | | More detailed error messages for Canonical Structure, #6398Gravatar Paul Steckler2018-02-06
| |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Maxime Dénès2018-02-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6695: [toplevel] Refine start of interactive mode conditions.Gravatar Maxime Dénès2018-02-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 23:06:07 +0000