aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-14Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵Gaëtan Gilbert
symlink from repo
2018-05-14Merge PR #7374: [sphinx] More fatal warnings.Maxime Dénès
2018-05-14Merge PR #7365: Mini fixes in the tactics chapterMaxime Dénès
2018-05-13Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoRalf Jung
Fixes #7065
2018-05-13Merge PR #7477: Support for notations with autonomous only-parsing and ↵Emilio Jesus Gallego Arias
only-printing declarations.
2018-05-13Merge PR #7489: gitlab CI: remove math-classes jobEmilio Jesus Gallego Arias
2018-05-11gitlab CI: remove math-classes jobGaëtan Gilbert
It's redundant as a dependency of formal-topology.
2018-05-11Merge PR #7340: Remove DirClosedSection.Enrico Tassi
2018-05-11Doc: Renaming an old-style numerical evar in an alphabetical one.Hugo Herbelin
2018-05-11Doc: Moving `\forall` to `forall` in file tactics.rst.Hugo Herbelin
Not only are most of "forall"s in the manual in Coq notation, but the math notation leads to have a specially long space after the comma.
2018-05-11Doc: Some quotes missing in file tactics.rst.Hugo Herbelin
2018-05-11Replacing a broken reference by hyperlinks in chapter tactics.Hugo Herbelin
2018-05-11A few fixes in chapter tactics.Hugo Herbelin
2018-05-11Merge PR #7470: use at least 6 Xs in mktemp filename templatesGaëtan Gilbert
2018-05-11Merge PR #6959: [build] Build checker generated files using a make rule.Enrico Tassi
2018-05-11Notations: advertize that distinct "only parsing"/"only printing" rules work.Hugo Herbelin
2018-05-11Merge PR #7466: Remove tutorials from the repoMaxime Dénès
2018-05-11Merge PR #7461: [sphinx] Improve the proof handling chapter.Maxime Dénès
2018-05-11Merge PR #7341: Don't recurse into closed modules/sections in split_lib.Enrico Tassi
2018-05-11Merge PR #7363: [ci] Fix another issue with the timing testsGaëtan Gilbert
2018-05-11Merge PR #7456: [toplevel] Don't ignore output filename provided by user in -oThéo Zimmermann
2018-05-10Merge PR #7437: [coqdep] Minor cleanups.Pierre-Marie Pédrot
2018-05-10Suggest going to /documentation to see a list of tutorials.Théo Zimmermann
2018-05-10One can build all the HTML doc using default.nix.Théo Zimmermann
2018-05-10Clean-up in Makefile.doc and include Sphinx in doc-html target.Théo Zimmermann
2018-05-10Remove tutorials.Théo Zimmermann
2018-05-10Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Hugo Herbelin
2018-05-10Fixes part 1 of #7462 (only-printing not to override existing interp rule).Hugo Herbelin
2018-05-10Merge PR #7473: [ci] Add mit-plv/cross-cryptoEmilio Jesus Gallego Arias
2018-05-10Merge PR #7471: [travis] Fix version of camlp5 for OCaml 4.06.1.Emilio Jesus Gallego Arias
2018-05-10[build] Build checker generated files using a make rule.Emilio Jesus Gallego Arias
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.
2018-05-09[ci] Add mit-plv/cross-cryptoJason Gross
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
2018-05-09[sphinx] Improve proof handling chapter.Théo Zimmermann
2018-05-09Clarify that the description of coqtop does not reflect all user interfaces.Théo Zimmermann
2018-05-09[sphinx] Improvements around the Show commands, including missing indices ↵Théo Zimmermann
and indentation.
2018-05-09[travis] Add explicit opam switch command to guarantee we're using the ↵Théo Zimmermann
requested compiler.
2018-05-09[travis] Fix version of camlp5 for OCaml 4.06.1.Théo Zimmermann
2018-05-09use at least 6 Xs in mktemp filename templatesSven M. Hallberg
OpenBSD mktemp fails with an error otherwise.
2018-05-09test for coqc -oEnrico Tassi
2018-05-09Merge PR #7438: [gitlab] Do expensive builds with the flambda compiled Coq.Gaëtan Gilbert
2018-05-09Merge PR #7435: [gitlab] Add bleeding-edge flambda build.Gaëtan Gilbert
2018-05-09[sphinx] Warn for dangling tacn / cmd / opt / ... references.Clément Pit-Claudel
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-09Replacing a broken reference by hyperlinks in chapter tactics.Hugo Herbelin
2018-05-09A few fixes in chapter tactics.Hugo Herbelin
2018-05-08Merge PR #7459: Try to fix CODEOWNERSThéo Zimmermann
2018-05-08Merge PR #7446: [lib] Re-add `set_timeout` to help users workaround #7408Pierre-Marie Pédrot
2018-05-08Try to fix CODEOWNERSMaxime Dénès
2018-05-08[gitlab] Do expensive builds with a flambda-compiled Coq.Emilio Jesus Gallego Arias
Gains seem superior to 50%, but data is taken from Gitlab so no reliable at all.
2018-05-08[CoqProject] Add some comments and remove unnecessary use of Pp.Emilio Jesus Gallego Arias
But indeed we need to split this file, as it is used now from CoqIDE is incorrect.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:33:09 +0000