Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | * | | | | | | | | | 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 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #6702: [vernac] [minor] Move print effects to top-level caller. | 2018-02-13 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode. | 2018-02-13 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking l... | 2018-02-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | ||||
* | | | | | | | | | | | Merge PR #6738: CHANGES for universe variance | 2018-02-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | * | [engine] Remove ghost parameter from `Proofview.Goal.t` | 2018-02-12 | ||
| | | | | | | | |_|_|/ | | | | | | | |/| | | | ||||
* | | | | | | | | | | | Merge PR #6565: [Backport script] Check .mli files are not changed. | 2018-02-12 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1082: Fixing Print for inductive types with let-in in parameters | 2018-02-12 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | ||||
| | | * | | | | | | | | | CHANGES for universe variance | 2018-02-12 | ||
| | | | | | | | * | | | | Add test case for #6677. | 2018-02-12 | ||
* | | | | | | | | | | | | Merge PR #6262: [error] Replace msg_error by a proper exception. | 2018-02-12 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | Merge PR #1047: Support universe instances on the literal Type | 2018-02-12 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6128: Simplification: cumulativity information is variance informa... | 2018-02-12 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception. | 2018-02-12 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | 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 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |