aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* More precise explanation when a notation is not reversible for printing.Gravatar Hugo Herbelin2018-02-20
* Adding support for re-folding notation referring to isolated "forall '(x,y), t".Gravatar Hugo Herbelin2018-02-20
* Again one more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2018-02-20
* Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Gravatar Maxime Dénès2018-02-19
|\
* \ Merge PR #6761: Remove unused argument in Record.declare_structureGravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\ \ \
* \ \ \ Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\ \ \ \
* \ \ \ \ Merge PR #6230: Better Cemitcodes API + compact relocation representationGravatar Maxime Dénès2018-02-19
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6759: detype_case predicate is not optionalGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6772: Cleanup inferCumulativityGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6648: [tactics] make apply_type safeGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ 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
|\ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 22:50:59 +0000