Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #6262: [error] Replace msg_error by a proper exception. | 2018-02-12 | |
|\ | |||
* \ | Merge PR #1047: Support universe instances on the literal Type | 2018-02-12 | |
|\ \ | |||
* \ \ | Merge PR #6128: Simplification: cumulativity information is variance informa... | 2018-02-12 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception. | 2018-02-12 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6418: More detailed error messages for Canonical Structure, #6398 | 2018-02-12 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6139: Make list functions returning sumbools transparent | 2018-02-12 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6718: Fix redirection to stderr in lint-repository error message. | 2018-02-12 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6708: Mention -quiet flag for Fail | 2018-02-12 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6706: ci-common: guess CI_BRANCH for local builds | 2018-02-12 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6651: Use r.(p) syntax to print primitive projections. | 2018-02-12 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6674: Delay computation of lifts in the reduction machine. | 2018-02-12 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | | | inferCumulativity: add comment to explain [if not is_arity]. | 2018-02-11 | |
| | | | | | | | | * | | | Documentation for cumulative inductive variance. | 2018-02-11 | |
| | | | | | | | | * | | | Print inductive cumulativity info in About. | 2018-02-11 | |
| | | | | | | | | * | | | Universe instance printer: add optional variance argument. | 2018-02-11 | |
| | | | | | | | | * | | | Use specialized function for inductive subtyping inference. | 2018-02-11 | |
| | | | | | | | | * | | | Inference of inductive subtyping does not need an evar map. | 2018-02-10 | |
| | | | | | | | | * | | | Simplification: cumulativity information is variance information. | 2018-02-10 | |
| | | | | | | | | * | | | [get_cumulativity_constraints] allowing further code sharing. | 2018-02-10 | |
| | | | | | | | | * | | | Factorize code for comparing maybe-cumulative inductives. | 2018-02-10 | |
| | | | | | | | | * | | | Fix typo in Univ.CumulativityInfo | 2018-02-10 | |
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | |||
| | | | | | | | | | * | [error] Replace msg_error by a proper exception. | 2018-02-09 | |
| | | | | | | | | |/ | | | | | | | | |/| | |||
| | | | | | | | * | | [nativecomp] Remove ad-hoc handling of Dynlink exception. | 2018-02-09 | |
| |_|_|_|_|_|_|/ / |/| | | | | | | | | |||
| | | | | * | | | | Fix redirection to stderr in lint-repository error message. | 2018-02-08 | |
| |_|_|_|/ / / / |/| | | | | | | | |||
| | | | * | | | | mention interactive mode for Fail message | 2018-02-07 | |
| |_|_|/ / / / |/| | | | | | | |||
* | | | | | | | Merge PR #6657: Document the Fail command | 2018-02-07 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6685: Use whd-all on rigid-flex conversion. | 2018-02-07 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6610: Points to Flocq official repository. | 2018-02-07 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding | 2018-02-07 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6673: Fix evar handling in native_compute conversion | 2018-02-07 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | | | ci-common: guess CI_BRANCH for local builds | 2018-02-07 | |
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | |||
| | | | | | | | | * | | More detailed error messages for Canonical Structure, #6398 | 2018-02-06 | |
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document. | 2018-02-06 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6695: [toplevel] Refine start of interactive mode conditions. | 2018-02-06 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | | | Points to Flocq official repository. | 2018-02-05 | |
| |_|_|_|/ / / / / / / |/| | | | | | | | | | | |||
| | | | | * | | | | | | Respect the transparent state of the current conversion on strong weak-head. | 2018-02-05 | |
| | | | * | | | | | | | Add overlay for equations (nf_beta takes an env) | 2018-02-05 | |
| | | * | | | | | | | | [native_compute] Fix handling of evars in conversion | 2018-02-05 | |
| | | * | | | | | | | | [native_compute] Remove useless conversion to list in reification. | 2018-02-05 | |
| |_|/ / / / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve... | 2018-02-05 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6654: CI: Run coqchk on Iris | 2018-02-05 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6652: Allow vernacular controls before focus selector | 2018-02-05 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | | | | [stm] [toplevel] Make loadpath a parameter of the document. | 2018-02-05 | |
| | | | |/ / / / / / / / | |||
| | | | * / / / / / / / | [toplevel] Refine start of interactive mode conditions. | 2018-02-05 | |
| |_|_|/ / / / / / / / |/| | | | | | | | | | | |||
| | | | | | | * | | | | Delay computation of lifts in the reduction machine. | 2018-02-04 | |
| |_|_|_|_|_|/ / / / |/| | | | | | | | | | |||
| | | | * | | | | | | CClosure.unfold_projection: don't catch Not_found, assume env is ok | 2018-02-02 | |
| | | | * | | | | | | Reductionops.nf_* now take an environment. | 2018-02-02 | |
| | | | * | | | | | | checker: cleanup projection unfolding | 2018-02-02 | |
| | | | * | | | | | | checker: remove unused per-constant reduction flags. | 2018-02-02 | |
| | | | * | | | | | | kernel: cleanup projection unfolding | 2018-02-02 | |
| |_|_|/ / / / / / |/| | | | | | | | |