aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* configure: fix warning printingGravatar Gaëtan Gilbert2018-06-03
* Merge PR #7683: [lib] Fix wrong deprecation annotations.Gravatar Pierre-Marie Pédrot2018-06-03
|\
* \ Merge PR #7656: CI for QuickChick and ext-libGravatar Emilio Jesus Gallego Arias2018-06-03
|\ \
| * | Update .gitlab to use newer ocamlGravatar Leonidas Lampropoulos2018-06-02
| | * [lib] Fix wrong deprecation annotations.Gravatar Emilio Jesus Gallego Arias2018-06-03
| |/ |/|
* | Merge PR #7681: Fixes #7636: location missing on deprecated compatibility not...Gravatar Emilio Jesus Gallego Arias2018-06-03
|\ \
| | * QuickChick CIGravatar Leonidas Lampropoulos2018-06-02
| |/ |/|
* | Merge PR #7680: [ci] Expose updated `OCAMLPATH` for CI users.Gravatar Gaëtan Gilbert2018-06-02
|\ \
| | * Fixes #7636: location missing on deprecated compatibility notations.Gravatar Hugo Herbelin2018-06-02
| |/ |/|
| * [ci] Expose updated `OCAMLPATH` for CI users.Gravatar Emilio Jesus Gallego Arias2018-06-02
* | Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \ | |/ |/|
* | Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.Gravatar Maxime Dénès2018-06-01
|\ \
* \ \ Merge PR #7537: Improve the Gallina chapter of the reference manual.Gravatar Maxime Dénès2018-06-01
|\ \ \
* \ \ \ Merge PR #7606: Allow more than one signature and name per Sphinx objectGravatar Maxime Dénès2018-06-01
|\ \ \ \
* \ \ \ \ Merge PR #7660: Add codeowner for timing python scriptsGravatar Maxime Dénès2018-06-01
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7652: Explicitly require python2 in python scripts in tools/Gravatar Jason Gross2018-05-31
|\ \ \ \ \ \
| | * | | | | Add codeowner for timing python scriptsGravatar Jason Gross2018-05-31
| |/ / / / / |/| | | | |
* | | | | | Merge PR #7401: Automatically run alienclean before compiling.Gravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \
| | * | | | | Explicitly require python2 in python scripts in tools/Gravatar Armaël Guéneau2018-05-31
| |/ / / / / |/| | | | |
| | | | * | [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
| | | | * | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
| |_|_|/ / |/| | | |
* | | | | Merge PR #6969: [api] Remove functions deprecated in 8.8Gravatar Maxime Dénès2018-05-31
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7564: Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Emilio Jesus Gallego Arias2018-05-31
|\ \ \ \ \ \
| | | | | | * Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
| |_|_|_|_|/ |/| | | | |
* | | | | | Merge PR #7578: Allow make clean to work on a fresh cloneGravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7639: Makefile: fix undefined NATIVEFILES when -native-compute noGravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7633: [Makefile] New target “install-merlin”Gravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \ \ \
| | | | * | | | | Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Gaëtan Gilbert2018-05-30
| |_|_|/ / / / / |/| | | | | | |
| | | | * | | | [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
| | | | * | | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | * | | | [api] Remove deprecated aliases from `Names`.Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | * | | | [api] Reintroduce `Names.global_reference` aliasGravatar Emilio Jesus Gallego Arias2018-05-30
| |_|_|/ / / / |/| | | | | |
* | | | | | | Merge PR #7260: Fix #6951: Unexpected error during scheme creation.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7621: Tactics.introduction: remove dangerous option ~checkGravatar Pierre-Marie Pédrot2018-05-30
|\ \ \ \ \ \ \ \ \
| | | | | * | | | | Makefile: fix undefined NATIVEFILES when -native-compute noGravatar Gaëtan Gilbert2018-05-30
| |_|_|_|/ / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #7593: Don't try to install native compiled files if native-compile ...Gravatar Maxime Dénès2018-05-29
|\ \ \ \ \ \ \ \ \
| | | | * | | | | | Fix #6951: Unexpected error during scheme creation.Gravatar Pierre-Marie Pédrot2018-05-29
| |_|_|/ / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #7566: Remove a dead old-refman file.Gravatar Maxime Dénès2018-05-29
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7628: [default.nix] Update dependency listGravatar Théo Zimmermann2018-05-29
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7626: Test for #7333 (soundness with VM/native and cofix)Gravatar Théo Zimmermann2018-05-29
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | | [Makefile] New target “install-merlin”Gravatar Vincent Laporte2018-05-29
| |_|_|_|_|_|/ / / / / |/| | | | | | | | | |
| | * | | | | | | | | [default.nix] Adds “ounit” to check dependenciesGravatar Vincent Laporte2018-05-29
| | * | | | | | | | | [default.nix] List “hostname” as a dependencyGravatar Vincent Laporte2018-05-29
| | * | | | | | | | | [default.nix] Use OCaml 4.06Gravatar Vincent Laporte2018-05-29
| | * | | | | | | | | [default.nix] Drop dependency to ocp-indexGravatar Vincent Laporte2018-05-29
| |/ / / / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #7084: [default.nix] Unpin nixpkgsGravatar Théo Zimmermann2018-05-29
|\ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | Add test for #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-29
| |/ / / / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #7521: Fix soundness bug with VM/native and cofixpointsGravatar Pierre-Marie Pédrot2018-05-28
|\ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | Tactics.introduction: remove dangerous option ~checkGravatar Enrico Tassi2018-05-28
| |_|_|_|/ / / / / / |/| | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 13:45:20 +0000