aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fixing a bug in printing the body of a located notation.Gravatar Hugo Herbelin2018-05-13
| | | | This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
* Removing a superfluous trailing newline in "Locate" for a notation.Gravatar Hugo Herbelin2018-05-13
|
* Merge PR #7477: Support for notations with autonomous only-parsing and ↵Gravatar Emilio Jesus Gallego Arias2018-05-13
|\ | | | | | | only-printing declarations.
* \ Merge PR #7489: gitlab CI: remove math-classes jobGravatar Emilio Jesus Gallego Arias2018-05-13
|\ \
| * | gitlab CI: remove math-classes jobGravatar Gaëtan Gilbert2018-05-11
| | | | | | | | | | | | It's redundant as a dependency of formal-topology.
* | | Merge PR #7340: Remove DirClosedSection.Gravatar Enrico Tassi2018-05-11
|\ \ \ | |/ / |/| |
* | | Merge PR #7470: use at least 6 Xs in mktemp filename templatesGravatar Gaëtan Gilbert2018-05-11
|\ \ \
* \ \ \ Merge PR #6959: [build] Build checker generated files using a make rule.Gravatar Enrico Tassi2018-05-11
|\ \ \ \
| | | | * Notations: advertize that distinct "only parsing"/"only printing" rules work.Gravatar Hugo Herbelin2018-05-11
| | | | |
* | | | | Merge PR #7466: Remove tutorials from the repoGravatar Maxime Dénès2018-05-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7461: [sphinx] Improve the proof handling chapter.Gravatar Maxime Dénès2018-05-11
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7341: Don't recurse into closed modules/sections in split_lib.Gravatar Enrico Tassi2018-05-11
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7363: [ci] Fix another issue with the timing testsGravatar Gaëtan Gilbert2018-05-11
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7456: [toplevel] Don't ignore output filename provided by user in -oGravatar Théo Zimmermann2018-05-11
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7437: [coqdep] Minor cleanups.Gravatar Pierre-Marie Pédrot2018-05-10
|\ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | Suggest going to /documentation to see a list of tutorials.Gravatar Théo Zimmermann2018-05-10
| | | | | | | | | | |
| | | | | | * | | | | One can build all the HTML doc using default.nix.Gravatar Théo Zimmermann2018-05-10
| | | | | | | | | | |
| | | | | | * | | | | Clean-up in Makefile.doc and include Sphinx in doc-html target.Gravatar Théo Zimmermann2018-05-10
| | | | | | | | | | |
| | | | | | * | | | | Remove tutorials.Gravatar Théo Zimmermann2018-05-10
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | | | | | | | * Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Gravatar Hugo Herbelin2018-05-10
| | | | | | | | | |
| | | | | | | | | * Fixes part 1 of #7462 (only-printing not to override existing interp rule).Gravatar Hugo Herbelin2018-05-10
| |_|_|_|_|_|_|_|/ |/| | | | | | | |
* | | | | | | | | Merge PR #7473: [ci] Add mit-plv/cross-cryptoGravatar Emilio Jesus Gallego Arias2018-05-10
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7471: [travis] Fix version of camlp5 for OCaml 4.06.1.Gravatar Emilio Jesus Gallego Arias2018-05-10
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | [build] Build checker generated files using a make rule.Gravatar Emilio Jesus Gallego Arias2018-05-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently, `configure.ml` does copy/link some files from `kernel` to `checker` in an ad-hoc way. Instead, it is preferable to add a copy rule to make and let it handle the dependencies properly. This also fixes a dependency bug in Windows, as files wouldn't be properly refreshed if `configure` was not run each time.
| | * | | | | | | | | [ci] Add mit-plv/cross-cryptoGravatar Jason Gross2018-05-09
| |/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
| | | | | | * | | | [sphinx] Improve proof handling chapter.Gravatar Théo Zimmermann2018-05-09
| | | | | | | | | |
| | | | | | * | | | Clarify that the description of coqtop does not reflect all user interfaces.Gravatar Théo Zimmermann2018-05-09
| | | | | | | | | |
| | | | | | * | | | [sphinx] Improvements around the Show commands, including missing indices ↵Gravatar Théo Zimmermann2018-05-09
| |_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | and indentation.
| * | | | | | | | [travis] Add explicit opam switch command to guarantee we're using the ↵Gravatar Théo Zimmermann2018-05-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | requested compiler.
| * | | | | | | | [travis] Fix version of camlp5 for OCaml 4.06.1.Gravatar Théo Zimmermann2018-05-09
|/ / / / / / / /
| | | | | | * / use at least 6 Xs in mktemp filename templatesGravatar Sven M. Hallberg2018-05-09
| |_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | OpenBSD mktemp fails with an error otherwise.
| | * | | | | test for coqc -oGravatar Enrico Tassi2018-05-09
| | | | | | |
* | | | | | | Merge PR #7438: [gitlab] Do expensive builds with the flambda compiled Coq.Gravatar Gaëtan Gilbert2018-05-09
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7435: [gitlab] Add bleeding-edge flambda build.Gravatar Gaëtan Gilbert2018-05-09
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7459: Try to fix CODEOWNERSGravatar Théo Zimmermann2018-05-08
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7446: [lib] Re-add `set_timeout` to help users workaround #7408Gravatar Pierre-Marie Pédrot2018-05-08
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
| | * | | | | | | | Try to fix CODEOWNERSGravatar Maxime Dénès2018-05-08
| |/ / / / / / / / |/| | | | | | | |
| | | * | | | | | [gitlab] Do expensive builds with a flambda-compiled Coq.Gravatar Emilio Jesus Gallego Arias2018-05-08
| | |/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Gains seem superior to 50%, but data is taken from Gitlab so no reliable at all.
| | | * | | | | [CoqProject] Add some comments and remove unnecessary use of Pp.Gravatar Emilio Jesus Gallego Arias2018-05-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | But indeed we need to split this file, as it is used now from CoqIDE is incorrect.
| | | * | | | | [coqdep] Remove unnecessary dependency on Pp and CError.Gravatar Emilio Jesus Gallego Arias2018-05-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows for even earlier bootstrapping.
| | | * | | | | [coqdep] Minor cleanups.Gravatar Emilio Jesus Gallego Arias2018-05-08
| |_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Remove inclusion of the `tactics` directory, this is coming from a time loadable modules were found there, now all are under `plugins`. - Remove 2 dependencies so we can bootstrap coqdep earlier. - Use `Format` instead of `Printf` for printing.
| | | * | | | [toplevel] Don't ignore output filename provided by user in -oGravatar Emilio Jesus Gallego Arias2018-05-08
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was a silly bug introduced in 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly forward the command line option. Thanks to @SkySkimmer for finding out the problem. closes #7447
| | * | | | [gitlab] Add bleeding-edge flambda build.Gravatar Emilio Jesus Gallego Arias2018-05-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We also introduce a bit more systematic job naming: `base/edge`. In order to make the flambda switch selectable we update the Docker image so all the dependencies are installed in that one. Note the extra quote rule for the flambda parameters, but unless we can assign arrays to Gitlab variables there is not a good way to do this I'm afraid. With this patch we are getting close to being able to remove most builds from Travis.
| * | | | | [lib] Re-add `set_timeout` to help users workaround #7408Gravatar Emilio Jesus Gallego Arias2018-05-07
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | It seems like #7408 will need some potentially intrusive work, so let's add the low-level hook back so third party developments can work well with `8.8.1/master` for the moment.
* | | | | Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging)Gravatar Maxime Dénès2018-05-07
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7371: Propose some updates of the CODEOWNER file.Gravatar Maxime Dénès2018-05-07
|\ \ \ \ \ \ | |_|/ / / / |/| | | | |
* | | | | | Merge PR #7445: [ci] Add ounit to the base Docker package set.Gravatar Gaëtan Gilbert2018-05-07
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7301: [sphinx] Backport forgotten updates during the migration & ↵Gravatar Maxime Dénès2018-05-07
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | other improvements
* \ \ \ \ \ \ \ Merge PR #7440: [ci] Add a default target to `Makefile.ci`Gravatar Gaëtan Gilbert2018-05-07
|\ \ \ \ \ \ \ \
| | | * | | | | | [ci] Add ounit to the base Docker package set.Gravatar Emilio Jesus Gallego Arias2018-05-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help #6808.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 11:49:40 +0000