aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
|\ \ \ \ \
* \ \ \ \ \ 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
| |_|_|_|/ / / / / / |/| | | | | | | | |
| | | | | | | | | * Improve the last section of the Gallina chapter.Gravatar Théo Zimmermann2018-05-28
| | | | | | | | | * Chapter 1 of the refman compiles without reporting any undocumented object.Gravatar Théo Zimmermann2018-05-28
| | | | | | | | | * Improve sections on (Co)Fixpoint of the Gallina chapter.Gravatar Théo Zimmermann2018-05-28
| * | | | | | | | | Add CHANGES entryGravatar Maxime Dénès2018-05-28
| * | | | | | | | | Fix #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-28
| * | | | | | | | | Unify pre_env and envGravatar Maxime Dénès2018-05-28
| * | | | | | | | | Remove vm_conv hook and reorganize kernel filesGravatar Maxime Dénès2018-05-28
| * | | | | | | | | Make some comments more precise about compilation of cofixpointsGravatar Maxime Dénès2018-05-28
| * | | | | | | | | Less confusing debug printing of setfield bytecode instructionGravatar Maxime Dénès2018-05-28
* | | | | | | | | | Merge PR #7419: Remove 100 occurrences of Evd.emptyGravatar Pierre-Marie Pédrot2018-05-28
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * Improve subsection on co-inductive types of the Gallina chapter.Gravatar Théo Zimmermann2018-05-27
| | | | | | * | | | | [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 16:47:21 +0000