| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | | | | | | | * | [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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | | | | | Points to Flocq official repository. |  Théo Zimmermann | 2018-02-05 | |
| | |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | | Respect the transparent state of the current conversion on strong weak-head. |  Pierre-Marie Pédrot | 2018-02-05 | |
| | | | | * | | | | | | | | | Add overlay for equations (nf_beta takes an env) | Gaëtan Gilbert | 2018-02-05 | |
| | | | * | | | | | | | | | | [native_compute] Fix handling of evars in conversion | Maxime Dénès | 2018-02-05 | |
| | | | * | | | | | | | | | | [native_compute] Remove useless conversion to list in reification. | Maxime Dénès | 2018-02-05 | |
| | |_|/ / / / / / / / / / |/| | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve... | Maxime Dénès | 2018-02-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6654: CI: Run coqchk on Iris | Maxime Dénès | 2018-02-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6652: Allow vernacular controls before focus selector | Maxime Dénès | 2018-02-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | | | | | | [stm] [toplevel] Make loadpath a parameter of the document. | Emilio Jesus Gallego Arias | 2018-02-05 | |
| | | | | |/ / / / / / / / / / | ||||
| | | | | * / / / / / / / / / | [toplevel] Refine start of interactive mode conditions. | Emilio Jesus Gallego Arias | 2018-02-05 | |
| | |_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | Delay computation of lifts in the reduction machine. | Pierre-Marie Pédrot | 2018-02-04 | |
| | |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | ||||
| | | | | * | | | | | | | | CClosure.unfold_projection: don't catch Not_found, assume env is ok | Gaëtan Gilbert | 2018-02-02 | |
| | | | | * | | | | | | | | Reductionops.nf_* now take an environment. | Gaëtan Gilbert | 2018-02-02 | |
| | | | | * | | | | | | | | checker: cleanup projection unfolding | Gaëtan Gilbert | 2018-02-02 | |
| | | | | * | | | | | | | | checker: remove unused per-constant reduction flags. | Gaëtan Gilbert | 2018-02-02 | |
| | | | | * | | | | | | | | kernel: cleanup projection unfolding | Gaëtan Gilbert | 2018-02-02 | |
| | |_|_|/ / / / / / / / |/| | | | | | | | | | | ||||
| | | | | * | | | | | | | Use whd-all on rigid-flex conversion. | Pierre-Marie Pédrot | 2018-02-02 | |
| | |_|_|/ / / / / / / |/| | | | | | | | | | ||||
| * | | | | | | | | | | Merge PR #6670: Delete duplicate line | Maxime Dénès | 2018-02-01 | |
| |\ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e... | Maxime Dénès | 2018-02-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6672: [stm] Move options to a per-document record. | Maxime Dénès | 2018-02-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6660: [lib] Respect change of options under with/without_option. | Maxime Dénès | 2018-02-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | | | | | | | [vernac] Mutual theorems (VernacStartTheoremProof) always have names |  Vincent Laporte | 2018-02-01 | |
| | | | | | | | * | | | | | | | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition | Vincent Laporte | 2018-02-01 | |
| | |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | CI: Run coqchk on Iris |  Ralf Jung | 2018-01-31 | |
| | | | * | | | | | | | | | | Proofview: enter_one: add __LOC__ argument to get relevant error msg |  Enrico Tassi | 2018-01-31 | |
| | | * | | | | | | | | | | | [stm] Move options to a per-document record. | Emilio Jesus Gallego Arias | 2018-01-31 | |
| | |/ / / / / / / / / / / |/| | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Merge PR #6601: Circle CI: fix cache selection. | Maxime Dénès | 2018-01-31 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing m... | Maxime Dénès | 2018-01-31 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6663: [toplevel] Refactor load path handling. | Maxime Dénès | 2018-01-31 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees" | Maxime Dénès | 2018-01-31 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | 2018-01-31 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | * | | | | | | | | | Delete duplicate line | Paul Steckler | 2018-01-30 | |
| | |_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | [lib] Respect change of options under with/without_option. | Emilio Jesus Gallego Arias | 2018-01-30 | |
| | |_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | Use r.(p) syntax to print primitive projections. | Maxime Dénès | 2018-01-30 | |
| | |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | Put default value for NJOBS in ci-common. | Gaëtan Gilbert | 2018-01-30 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |