| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | | | | * | | | | | Adding a sanity check on inductive variance subtyping. |  Pierre-Marie Pédrot | 2018-02-15 | |
| | |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | [toplevel] Make toplevel state into a record. |  Emilio Jesus Gallego Arias | 2018-02-15 | |
| | | | | | | | * | | | | | | | [ide] Localize a IDE-specific flag. | Emilio Jesus Gallego Arias | 2018-02-15 | |
| | |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | Merge PR #1073: new quick2vo target: like vio2vo, but smarter |  Maxime Dénès | 2018-02-15 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | disable tests: vio2vo is broken in Windows |  Ralf Jung | 2018-02-15 | |
| | * | | | | | | | | | | | | | also test vio2vo | Ralf Jung | 2018-02-15 | |
| | * | | | | | | | | | | | | | test "make quick2vo" | Ralf Jung | 2018-02-15 | |
| | * | | | | | | | | | | | | | new quick2vo target: like vio2vo, but smarter | Ralf Jung | 2018-02-15 | |
| | | |_|_|/ / / / / / / / / | |/| | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject | Maxime Dénès | 2018-02-15 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | coq_makefile: Support "" as the prefix in _CoqProject |  Joachim Breitner | 2018-02-15 | |
| * | | | | | | | | | | | | | | Merge PR #6760: CHANGES for 8.7.2. | Maxime Dénès | 2018-02-15 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | * | Extend `zify_N` with knowledge about `N.pred` | Joachim Breitner | 2018-02-14 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | CHANGES for 8.7.2. |  Théo Zimmermann | 2018-02-14 | |
| |/ / / / / / / / / / / / / | ||||
| | | | | | | | | | * / / / | Remove unused argument in Record.declare_structure |  Gaëtan Gilbert | 2018-02-14 | |
| | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | ||||
| | | | | | | | * | | | | | Factorize the relocations in the on-disk VM representation. | Pierre-Marie Pédrot | 2018-02-14 | |
| | | | | | | | * | | | | | Use a more compact representation for bytecode relocations stored on disk. | Pierre-Marie Pédrot | 2018-02-14 | |
| | | | | | | | * | | | | | Do not use global variables for VM bytecode compilation in Cemitcodes. | Pierre-Marie Pédrot | 2018-02-14 | |
| | | | | | | | * | | | | | Remove the unsafe bytes conversion function in Cemitcodes. | Pierre-Marie Pédrot | 2018-02-14 | |
| | | | | | | | * | | | | | Move the call to the computation of bytecode inside Cemitcodes. | Pierre-Marie Pédrot | 2018-02-14 | |
| | | | | | | | * | | | | | Abstract further the type of VM bytecode compilation. | Pierre-Marie Pédrot | 2018-02-14 | |
| | |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | ||||
| | | | | | | * | | | | | detype_case predicate is not optional | Gaëtan Gilbert | 2018-02-14 | |
| * | | | | | | | | | | | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation) | Maxime Dénès | 2018-02-14 | |
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6713: Fix #6677: Critical bug with VM and universes | Maxime Dénès | 2018-02-14 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | ||||
| | | | | | | * | | | | | | [build] Fix VM dynamic linking prep in byte builds. | Emilio Jesus Gallego Arias | 2018-02-14 | |
| | | | | |_|/ / / / / / | | | |/| | | | | | | | ||||
| | | | | | | * | | | | | coqdev.el: wait for 'compile to touch compilation-error-regexp-alist | Gaëtan Gilbert | 2018-02-13 | |
| | | * | | | | | | | | | Add CHANGES entry for #1047 |  Tej Chajed | 2018-02-13 | |
| | | |/ / / / / / / / | ||||
| | | | | | * | | | | | coqdev.el: fix "compilate"-command typo | Gaëtan Gilbert | 2018-02-13 | |
| | | | | | * | | | | | coqdev.el: shell-quote-argument the directory for make -C | Gaëtan Gilbert | 2018-02-13 | |
| | | | | | * | | | | | coqdev.el: stop using when-let for emacs<25 compatibility. | Gaëtan Gilbert | 2018-02-13 | |
| * | | | | | | | | | | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | * | | | [engine] Remove ghost parameter from `Proofview.Goal.t` | Emilio Jesus Gallego Arias | 2018-02-12 | |
| | | | | | | | | |_|_|/ / / | | | | | | | |/| | | | | | ||||
| * | | | | | | | | | | | | | 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 | |
| | | | | | | | | * | | | | | | Add test case for #6677. | Maxime Dénès | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |