Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Fix #6529: nf_evar_info and check the env evars' not just the concl | Matthieu Sozeau | 2018-02-19 |
* | Merge PR #6693: [toplevel] Refactor command line argument handling. | Maxime Dénès | 2018-02-13 |
|\ | |||
* \ | Merge PR #6702: [vernac] [minor] Move print effects to top-level caller. | Maxime Dénès | 2018-02-13 |
|\ \ | |||
* \ \ | Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode. | Maxime Dénès | 2018-02-13 |
|\ \ \ | |||
* \ \ \ | Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking l... | Maxime Dénès | 2018-02-13 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6738: CHANGES for universe variance | Maxime Dénès | 2018-02-13 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6565: [Backport script] Check .mli files are not changed. | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #1082: Fixing Print for inductive types with let-in in parameters | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ | |||
| | | * | | | | | CHANGES for universe variance | Gaëtan Gilbert | 2018-02-12 |
* | | | | | | | | Merge PR #6262: [error] Replace msg_error by a proper exception. | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ | |_|_|/ / / / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #1047: Support universe instances on the literal Type | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6128: Simplification: cumulativity information is variance informa... | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception. | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6418: More detailed error messages for Canonical Structure, #6398 | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6139: Make list functions returning sumbools transparent | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6718: Fix redirection to stderr in lint-repository error message. | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6708: Mention -quiet flag for Fail | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6706: ci-common: guess CI_BRANCH for local builds | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6651: Use r.(p) syntax to print primitive projections. | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6674: Delay computation of lifts in the reduction machine. | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | | | | | | | | | inferCumulativity: add comment to explain [if not is_arity]. | Gaëtan Gilbert | 2018-02-11 |
| | | | | | | | | * | | | | | | | | | Documentation for cumulative inductive variance. | Gaëtan Gilbert | 2018-02-11 |
| | | | | | | | | * | | | | | | | | | Print inductive cumulativity info in About. | Gaëtan Gilbert | 2018-02-11 |
| | | | | | | | | * | | | | | | | | | Universe instance printer: add optional variance argument. | Gaëtan Gilbert | 2018-02-11 |
| | | | | | | | | * | | | | | | | | | Use specialized function for inductive subtyping inference. | Gaëtan Gilbert | 2018-02-11 |
| | | | | | | | | * | | | | | | | | | Inference of inductive subtyping does not need an evar map. | Gaëtan Gilbert | 2018-02-10 |
| | | | | | | | | * | | | | | | | | | Simplification: cumulativity information is variance information. | Gaëtan Gilbert | 2018-02-10 |
| | | | | | | | | * | | | | | | | | | [get_cumulativity_constraints] allowing further code sharing. | Gaëtan Gilbert | 2018-02-10 |
| | | | | | | | | * | | | | | | | | | Factorize code for comparing maybe-cumulative inductives. | Gaëtan Gilbert | 2018-02-10 |
| | | | | | | | | * | | | | | | | | | Fix typo in Univ.CumulativityInfo | Gaëtan Gilbert | 2018-02-10 |
| |_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | * | | [vernac] Fix outdated comment. | Emilio Jesus Gallego Arias | 2018-02-09 |
| | | | | | | | | | | | | | | * | | [nit] Remove some unnecessary global `open Feedback` | Emilio Jesus Gallego Arias | 2018-02-09 |
| | | | | | | | | | | | | | | * | | [vernac] [minor] Move print effects to top-level caller. | Emilio Jesus Gallego Arias | 2018-02-09 |
| | | | | | | | | | | |_|_|_|/ / | | | | | | | | | | |/| | | | | | |||
| | | | | | | | | | * | | | | | | [error] Replace msg_error by a proper exception. | Emilio Jesus Gallego Arias | 2018-02-09 |
| | | | | | | | | |/ / / / / / | | | | | | | | |/| | | | | | | |||
| | | | | | | | * | | | | | | | [nativecomp] Remove ad-hoc handling of Dynlink exception. | Emilio Jesus Gallego Arias | 2018-02-09 |
| |_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | [toplevel] Small refactoring of fatal_error functions. | Emilio Jesus Gallego Arias | 2018-02-09 |
| | | | | | | | | | | | | * | [toplevel] Refactor command line argument handling. | Emilio Jesus Gallego Arias | 2018-02-09 |
| | | | | | | | | | | | |/ | |||
| | | | | * | | | | | | / | Fix redirection to stderr in lint-repository error message. | Gaëtan Gilbert | 2018-02-08 |
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | | | |||
| | | | * | | | | | | | | mention interactive mode for Fail message | Paul Steckler | 2018-02-07 |
| |_|_|/ / / / / / / / |/| | | | | | | | | | | |||
| | | | | | | | | | * | [toplevel] Disable error resiliency in `-quick` mode. | Emilio Jesus Gallego Arias | 2018-02-07 |
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #6657: Document the Fail command | Maxime Dénès | 2018-02-07 |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6685: Use whd-all on rigid-flex conversion. | Maxime Dénès | 2018-02-07 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6610: Points to Flocq official repository. | Maxime Dénès | 2018-02-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding | Maxime Dénès | 2018-02-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6673: Fix evar handling in native_compute conversion | Maxime Dénès | 2018-02-07 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | | | | | | ci-common: guess CI_BRANCH for local builds | Gaëtan Gilbert | 2018-02-07 |
| |_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Possible fix for issue #6697 | Yannick Forster | 2018-02-07 |
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | |||
| | | | | | | | | * | | | | More detailed error messages for Canonical Structure, #6398 | Paul Steckler | 2018-02-06 |
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | |||
* | | | | | | | | | | | | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document. | Maxime Dénès | 2018-02-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6695: [toplevel] Refine start of interactive mode conditions. | Maxime Dénès | 2018-02-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ |