aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* | | | | | | | | | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6571: Fix ci-all targetGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | * | | | | | | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | * | | | | | | | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
| | | | | * | | | | | | Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| | | | | * | | | | | | Fix reduction flags in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| |_|_|_|/ / / / / / / |/| | | | | | | | | |
| | | | | | | | | | * Adding a test for the construction that was broken in Coccinelle.Gravatar Pierre-Marie Pédrot2018-02-16
| | | | | | | | | | * Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | |
| | | | | | | * | | [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
| | | | | | | * | | [ide] Localize a IDE-specific flag.Gravatar Emilio Jesus Gallego Arias2018-02-15
| |_|_|_|_|_|/ / / |/| | | | | | | |
* | | | | | | | | Merge PR #1073: new quick2vo target: like vio2vo, but smarterGravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | disable tests: vio2vo is broken in WindowsGravatar Ralf Jung2018-02-15
| * | | | | | | | | also test vio2voGravatar Ralf Jung2018-02-15
| * | | | | | | | | test "make quick2vo"Gravatar Ralf Jung2018-02-15
| * | | | | | | | | new quick2vo target: like vio2vo, but smarterGravatar Ralf Jung2018-02-15
| | |_|_|/ / / / / | |/| | | | | | |
* | | | | | | | | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectGravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | coq_makefile: Support "" as the prefix in _CoqProjectGravatar Joachim Breitner2018-02-15
* | | | | | | | | | Merge PR #6760: CHANGES for 8.7.2.Gravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | CHANGES for 8.7.2.Gravatar Théo Zimmermann2018-02-14
|/ / / / / / / / / /
| | | | | | | | | * Remove unused argument in Record.declare_structureGravatar Gaëtan Gilbert2018-02-14
| |_|_|_|_|_|_|_|/ |/| | | | | | | |
| | | | | | | * | Factorize the relocations in the on-disk VM representation.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | * | Use a more compact representation for bytecode relocations stored on disk.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | * | Do not use global variables for VM bytecode compilation in Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | * | Remove the unsafe bytes conversion function in Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | * | Move the call to the computation of bytecode inside Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
| | | | | | | * | Abstract further the type of VM bytecode compilation.Gravatar Pierre-Marie Pédrot2018-02-14
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | | | * | detype_case predicate is not optionalGravatar Gaëtan Gilbert2018-02-14
* | | | | | | | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Gravatar Maxime Dénès2018-02-14
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6713: Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-14
|\ \ \ \ \ \ \ \ \
| | | | | | * | | | [build] Fix VM dynamic linking prep in byte builds.Gravatar Emilio Jesus Gallego Arias2018-02-14
| | | | |_|/ / / / | | | |/| | | | |
| | | | | | * | | coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGravatar Gaëtan Gilbert2018-02-13
| | * | | | | | | Add CHANGES entry for #1047Gravatar Tej Chajed2018-02-13
| | |/ / / / / /
| | | | | * | | coqdev.el: fix "compilate"-command typoGravatar Gaëtan Gilbert2018-02-13
| | | | | * | | coqdev.el: shell-quote-argument the directory for make -CGravatar Gaëtan Gilbert2018-02-13
| | | | | * | | coqdev.el: stop using when-let for emacs<25 compatibility.Gravatar Gaëtan Gilbert2018-02-13
* | | | | | | | Merge PR #6693: [toplevel] Refactor command line argument handling.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode.Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking l...Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #6738: CHANGES for universe varianceGravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| | | | | | | | |_|_|/ | | | | | | | |/| | |
* | | | | | | | | | | Merge PR #6565: [Backport script] Check .mli files are not changed.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | * | | | | | | | | CHANGES for universe varianceGravatar Gaëtan Gilbert2018-02-12
| | | | | | | | * | | | Add test case for #6677.Gravatar Maxime Dénès2018-02-12
* | | | | | | | | | | | Merge PR #6262: [error] Replace msg_error by a proper exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6128: Simplification: cumulativity information is variance informa...Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 06:38:45 +0000