Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | | | | | | | | | 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 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | * | | | Fix #6677: Critical bug with VM and universes | 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 | ||
| | | | | | | | | | | | | | | | | | | * | Merge anomaly-traces-parser.el into coqdev.el. | 2018-02-11 | ||
| | | | | | | | | | | | | | | | | | | * | coqdev.el: add installation instructions. | 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 | ||
| |_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | | [vernac] Fix outdated comment. | 2018-02-09 | ||
| | | | | | | | | | | | | | | * | | | | [nit] Remove some unnecessary global `open Feedback` | 2018-02-09 | ||
| | | | | | | | | | | | | | | * | | | | [vernac] [minor] Move print effects to top-level caller. | 2018-02-09 | ||
| | | | | | | | | | | |_|_|_|/ / / / | | | | | | | | | | |/| | | | | | | | ||||
| | | | | | | | | | * | | | | | | | | [error] Replace msg_error by a proper exception. | 2018-02-09 | ||
| | | | | | | | | |/ / / / / / / / | | | | | | | | |/| | | | | | | | | ||||
| | | | | | | | * | | | | | | | | | [nativecomp] Remove ad-hoc handling of Dynlink exception. | 2018-02-09 | ||
| |_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | [toplevel] Small refactoring of fatal_error functions. | 2018-02-09 | ||
| | | | | | | | | | | | | * | | | [toplevel] Refactor command line argument handling. | 2018-02-09 | ||
| | | | | | | | | | | | |/ / / | ||||
| | | | | * | | | | | | / / / | Fix redirection to stderr in lint-repository error message. | 2018-02-08 | ||
| |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | mention interactive mode for Fail message | 2018-02-07 | ||
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | [toplevel] Disable error resiliency in `-quick` mode. | 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 | ||
| |_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | Possible fix for issue #6697 | 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 | ||
| |_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | |