Commit message (Expand) | Author | Age | |
---|---|---|---|
* | [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 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | 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 | |
| |_|_|/ / / / |/| | | | | | | |||
| | | | * | | | 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 | |
| |_|_|/ / / |/| | | | | | |||
| | | | * | | Use whd-all on rigid-flex conversion. | 2018-02-02 | |
| |_|_|/ / |/| | | | | |||
* | | | | | Merge PR #6670: Delete duplicate line | 2018-02-01 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e... | 2018-02-01 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6672: [stm] Move options to a per-document record. | 2018-02-01 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6660: [lib] Respect change of options under with/without_option. | 2018-02-01 | |
|\ \ \ \ \ \ \ \ | |||
| | | | | | | * | | [vernac] Mutual theorems (VernacStartTheoremProof) always have names | 2018-02-01 | |
| | | | | | | * | | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition | 2018-02-01 | |
| |_|_|_|_|_|/ / |/| | | | | | | | |||
| | | | | | * | | CI: Run coqchk on Iris | 2018-01-31 | |
| | | * | | | | | Proofview: enter_one: add __LOC__ argument to get relevant error msg | 2018-01-31 | |
| | * | | | | | | [stm] Move options to a per-document record. | 2018-01-31 | |
| |/ / / / / / |/| | | | | | | |||
* | | | | | | | Merge PR #6601: Circle CI: fix cache selection. | 2018-01-31 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing m... | 2018-01-31 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6663: [toplevel] Refactor load path handling. | 2018-01-31 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees" | 2018-01-31 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | 2018-01-31 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | | | Delete duplicate line | 2018-01-30 | |
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | |||
| | | | | | * | | | | | [lib] Respect change of options under with/without_option. | 2018-01-30 | |
| |_|_|_|_|/ / / / / |/| | | | | | | | | | |||
| | | | * | | | | | | Put default value for NJOBS in ci-common. | 2018-01-30 | |
| * | | | | | | | | | Adding an overlay for Equations. | 2018-01-30 | |
* | | | | | | | | | | Merge PR #6666: Fix reduction of primitive projections on coinductive records... | 2018-01-30 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projections | 2018-01-30 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6636: Stop running duplicate Travis jobs on pull requests. | 2018-01-30 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6605: Safer VM interfaces | 2018-01-30 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6644: Use travis_retry on apt-get update | 2018-01-30 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | Add test case for #5286. | 2018-01-29 | |
| | | | | * | | | | | | | | | [cbv] Fix evaluation of cofixpoints under primitive projections. | 2018-01-29 | |
| | | | | * | | | | | | | | | [native_compute] Fix evaluation of cofixpoints under primitive projections. | 2018-01-29 | |
| |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | |