Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Update CREDITS. | 2018-02-21 | |
* | More accurate and complete headers. | 2018-02-21 | |
* | Mention the CREDITS file in CONTRIBUTING. | 2018-02-21 | |
* | Remove redundant COPYRIGHT file. | 2018-02-21 | |
* | Merge PR #6728: Extrude monomorphic universe contexts from with Definition co... | 2018-02-19 | |
|\ | |||
* \ | Merge PR #6761: Remove unused argument in Record.declare_structure | 2018-02-19 | |
|\ \ | |||
* \ \ | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t` | 2018-02-19 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6753: [toplevel] Make toplevel state into a record. | 2018-02-19 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6230: Better Cemitcodes API + compact relocation representation | 2018-02-19 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6759: detype_case predicate is not optional | 2018-02-19 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6772: Cleanup inferCumulativity | 2018-02-19 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6648: [tactics] make apply_type safe | 2018-02-19 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ... | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead. | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds. | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6571: Fix ci-all target | 2018-02-19 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | 2018-02-17 | |
| | | | | * | | | | | | | | apply_type: add option "typecheck" passed down to refine | 2018-02-16 | |
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | | | |||
| | | | | * | | | | | | | Cleaner treatment of parameters in inferCumulativity | 2018-02-16 | |
| | | | | * | | | | | | | Fix reduction flags in inferCumulativity | 2018-02-16 | |
| |_|_|_|/ / / / / / / |/| | | | | | | | | | | |||
| | | | | | | | | | * | Adding a test for the construction that was broken in Coccinelle. | 2018-02-16 | |
| | | | | | | | | | * | Extrude monomorphic universe contexts from with Definition constraints. | 2018-02-16 | |
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |||
| | | | | | | * | | | [toplevel] Make toplevel state into a record. | 2018-02-15 | |
| | | | | | | * | | | [ide] Localize a IDE-specific flag. | 2018-02-15 | |
| |_|_|_|_|_|/ / / |/| | | | | | | | | |||
* | | | | | | | | | Merge PR #1073: new quick2vo target: like vio2vo, but smarter | 2018-02-15 | |
|\ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | disable tests: vio2vo is broken in Windows | 2018-02-15 | |
| * | | | | | | | | | also test vio2vo | 2018-02-15 | |
| * | | | | | | | | | test "make quick2vo" | 2018-02-15 | |
| * | | | | | | | | | new quick2vo target: like vio2vo, but smarter | 2018-02-15 | |
| | |_|_|/ / / / / | |/| | | | | | | | |||
* | | | | | | | | | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject | 2018-02-15 | |
|\ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | coq_makefile: Support "" as the prefix in _CoqProject | 2018-02-15 | |
* | | | | | | | | | | Merge PR #6760: CHANGES for 8.7.2. | 2018-02-15 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | CHANGES for 8.7.2. | 2018-02-14 | |
|/ / / / / / / / / / | |||
| | | | | | | | | * | Remove unused argument in Record.declare_structure | 2018-02-14 | |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
| | | | | | | * | | Factorize the relocations in the on-disk VM representation. | 2018-02-14 | |
| | | | | | | * | | Use a more compact representation for bytecode relocations stored on disk. | 2018-02-14 | |
| | | | | | | * | | Do not use global variables for VM bytecode compilation in Cemitcodes. | 2018-02-14 | |
| | | | | | | * | | Remove the unsafe bytes conversion function in Cemitcodes. | 2018-02-14 | |
| | | | | | | * | | Move the call to the computation of bytecode inside Cemitcodes. | 2018-02-14 | |
| | | | | | | * | | Abstract further the type of VM bytecode compilation. | 2018-02-14 | |
| |_|_|_|_|_|/ / |/| | | | | | | | |||
| | | | | | * | | detype_case predicate is not optional | 2018-02-14 | |
* | | | | | | | | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation) | 2018-02-14 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6713: Fix #6677: Critical bug with VM and universes | 2018-02-14 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | [build] Fix VM dynamic linking prep in byte builds. | 2018-02-14 | |
| | | | |_|/ / / / | | | |/| | | | | | |||
| | | | | | * | | | coqdev.el: wait for 'compile to touch compilation-error-regexp-alist | 2018-02-13 | |
| | * | | | | | | | Add CHANGES entry for #1047 | 2018-02-13 | |
| | |/ / / / / / | |||
| | | | | * | | | coqdev.el: fix "compilate"-command typo | 2018-02-13 | |
| | | | | * | | | coqdev.el: shell-quote-argument the directory for make -C | 2018-02-13 | |
| | | | | * | | | coqdev.el: stop using when-let for emacs<25 compatibility. | 2018-02-13 | |
* | | | | | | | | Merge PR #6693: [toplevel] Refactor command line argument handling. | 2018-02-13 | |
|\ \ \ \ \ \ \ \ |