aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Remove dead code that used to be there for CamlpX compatibility.Gravatar Pierre-Marie Pédrot2018-07-07
| | | | | | Part of this code has been introduced very recently in 7c62654 in spite of the existence of a proper API. This means that this should be better documented.
* Merge PR #8005: Fix compilation of Coq with camlp5 master branch.Gravatar Emilio Jesus Gallego Arias2018-07-07
|\
* \ Merge PR #8001: Cache the build of the Nix package using Cachix.Gravatar Gaëtan Gilbert2018-07-06
|\ \
* \ \ Merge PR #7821: [refine] obey the use_unification_heuristics flagGravatar Pierre-Marie Pédrot2018-07-06
|\ \ \
* \ \ \ Merge PR #8008: Add test for #8004.Gravatar Théo Zimmermann2018-07-06
|\ \ \ \
| | | * | [pkg:nix] Add more comments and allow overriding extra substituters.Gravatar Théo Zimmermann2018-07-06
| | | | |
| * | | | Add test for #8004.Gravatar Gaëtan Gilbert2018-07-06
|/ / / /
| | | * Fix compilation of Coq with camlp5 master branch.Gravatar Pierre-Marie Pédrot2018-07-06
| |_|/ |/| | | | | | | | | | | There was a conflict in the name of an exported function. A good argument in favour of PR #7898.
* | | Merge PR #7990: Convert timing tool to python3Gravatar Jason Gross2018-07-05
|\ \ \
| | * | refine: obey the use_unification_heuristics flagGravatar Matthieu Sozeau2018-07-05
| |/ / |/| |
* | | Merge PR #7991: Make Travis faster by removing more builds.Gravatar Emilio Jesus Gallego Arias2018-07-05
|\ \ \
* \ \ \ Merge PR #7994: Make bin/ in makefile, not configure.Gravatar Emilio Jesus Gallego Arias2018-07-05
|\ \ \ \
| | | | * [pkg:nix] Stop using lib.inNixShell.Gravatar Théo Zimmermann2018-07-05
| | | | |
| | | | * [pkg:nix] Change the download method.Gravatar Théo Zimmermann2018-07-05
| | | | | | | | | | | | | | | | | | | | | | | | | This will allow for better reuse of the cache when the URL is different but the archive is the same.
| | | | * [pkg:nix] Pass through the ocamlPackages version used to build.Gravatar Théo Zimmermann2018-07-05
| | | | | | | | | | | | | | | | | | | | This will be useful for users wanting to build a plugin using this package.
| | | | * [pkg:nix] Cache the build using Cachix when signing key is set.Gravatar Théo Zimmermann2018-07-05
| |_|_|/ |/| | |
| | * | Remove some Travis jobs to make the build faster.Gravatar Théo Zimmermann2018-07-05
| |/ / |/| |
* | | Merge PR #7746: Many small cleanups removing unused arguments and functionsGravatar Pierre-Marie Pédrot2018-07-05
|\ \ \
* \ \ \ Merge PR #7979: TACTIC EXTEND in coqppGravatar Emilio Jesus Gallego Arias2018-07-05
|\ \ \ \
* \ \ \ \ Merge PR #7973: Add a test build on NixOS to GitLab CI.Gravatar Gaëtan Gilbert2018-07-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7989: [ci] Avoid annoying detached head warning.Gravatar Gaëtan Gilbert2018-07-04
|\ \ \ \ \ \
| | | | | | * Convert timing tools to run with both python2 and python3Gravatar Jasper Hugunin2018-07-04
| | | | | | |
* | | | | | | Merge PR #7993: doc: Fix markup in Calculus of Inductive ConstructionsGravatar Théo Zimmermann2018-07-04
|\ \ \ \ \ \ \
| * | | | | | | doc: Fix markup in Calculus of Inductive ConstructionsGravatar Fabian2018-07-04
| | |_|_|_|_|/ | |/| | | | |
* | | | | | | Merge PR #7992: Print something after the build completed if it wasn't a ↵Gravatar Gaëtan Gilbert2018-07-04
|\ \ \ \ \ \ \ | |/ / / / / / |/| | | | | | | | | | | | | runner failure.
| * | | | | | Print something after the build completed if it wasn't a runner failure.Gravatar Théo Zimmermann2018-07-04
|/ / / / / / | | | | | | | | | | | | | | | | | | This can then be leveraged by @coqbot to know which builds to restart.
| * / / / / [ci] Avoid annoying detached head warning.Gravatar Emilio Jesus Gallego Arias2018-07-04
|/ / / / /
| | | | * Make bin/ in makefile, not configure.Gravatar Gaëtan Gilbert2018-07-04
| |_|_|/ |/| | |
| * | | Add a shell.nix that is not pinned to satisfy some developers' preference.Gravatar Théo Zimmermann2018-07-03
| | | |
| * | | Refactor default.nix to use optionals.Gravatar Théo Zimmermann2018-07-03
| | | |
| * | | Fix timing tools on NixOS.Gravatar Théo Zimmermann2018-07-03
| | | |
| * | | Add a test build of Nix package to GitLab CI.Gravatar Théo Zimmermann2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | We pin default.nix again to make the CI build predictable. As in Windows builds, we need to override the default before_script. As in other test-suite jobs, we export logs as artifacts on failure.
| * | | Adapt default.nix to allow nix-build to run the test-suite.Gravatar Théo Zimmermann2018-07-03
|/ / /
* | | Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵Gravatar Gaëtan Gilbert2018-07-03
|\ \ \ | | | | | | | | | | | | with apt.
| | | * Add overlay for equations.Gravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Library: use ocaml typing to show that we find at most 2 filesGravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Library.register_loaded_library: remove unused variableGravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | | | | | | | | | This one is a bit weird. Unused since 4d95eb4e878f375a69f1b48d8833801bf555fdd0 (kept semantics, the m is the same one outside and inside the call)
| | | * Glob_ops.rename_glob_vars: fix typoGravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Glob_ops.fix_kind_eq: fix typoGravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Pputils: fix typoGravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Evarutil.(e_)new_Type: remove unused env argumentGravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Remove unused function Evd.whd_sort_variableGravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Remove unused output of Universes.normalize_univ_variablesGravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | (Universes and Evd)
| | | * Coq_omega: remove unused Goal.entersGravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
| | | * Remove unused function Coq_omega.timing.Gravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Taccoerce: remove various unused arguments.Gravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * Remove unused arguments to Ide_slave.concl_next_tac.Gravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | | | | | Unused since 2285dae8af54043090ce5f8a59aa4162679714c6
| | | * Pptactic: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | |
| | | * checker Indtypes: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 23:56:27 +0000