aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
This API is a bit strange, I expect it will change at some point.
2018-05-17Stop using Universes.subst(_opt)_univs_constrGaëtan Gilbert
Should it be removed? The underlying `universe_subst -> constr -> constr` seems like it could be useful for plugins but where would the substitution be from?
2018-05-17Make set minimization option internal to UniversesGaëtan Gilbert
2018-05-17[circle] Use Docker image from Gitlab registry.Emilio Jesus Gallego Arias
2018-05-17Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵Emilio Jesus Gallego Arias
by default.
2018-05-17Merge PR #7359: Reduce usage of evar_map referencesPierre-Marie Pédrot
2018-05-17[tuto2] Clarify where the name of the ML plugin is usedEnrico Tassi
2018-05-17add little testEnrico Tassi
- tests the plugin can actually be loaded (eg with the wrong DECLARE PLUGIN it loads but then the tactic is not in scope) - sine is listed in _CoqProject one can open it with CoqIDE/PG and get the -I -R flags from the _CoqProject automatically
2018-05-17DECLARE PLUGIN "$name" === Declare ML Module "$name"Enrico Tassi
2018-05-17Add some setup instructionsEnrico
2018-05-17Merge pull request #2 from gares/gares-patch-1Yves Bertot
[tuto1] Minor fixes to comments
2018-05-17[tuto1] Minor fixes to commentsEnrico
2018-05-17Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in ↵Pierre-Marie Pédrot
`comDefinition`.
2018-05-17Merge PR #6870: [ide] Don't set `quiet` on start.Enrico Tassi
2018-05-17Merge PR #7525: [ci] Try to build more of fiat-crypto.Gaëtan Gilbert
2018-05-17Merge PR #6808: Add unit tests to test-suiteGaëtan Gilbert
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-17[STM] Nested Proofs Allowed has to be executed immediatelyEnrico Tassi
since it affects scheduling (actually the error the option lets one silence)
2018-05-17Remove deprecation warning for nested proofs.Théo Zimmermann
It is not clear yet that support for nested proofs will actually get removed in a future version.
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-16Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.Maxime Dénès
2018-05-16Modify make system to include Makefile.common in the test suiteGaëtan Gilbert
2018-05-16[ci] Try to build more of fiat-crypto.Emilio Jesus Gallego Arias
2018-05-16Merge PR #7514: [ci] Don't build lite versions of CI developments.Gaëtan Gilbert
2018-05-16Merge PR #7535: Typo in documentation of DeriveThéo Zimmermann
2018-05-16Merge PR #7493: Minor update of the documentation about the rcfileEmilio Jesus Gallego Arias
2018-05-16Typo in documentation of DeriveJoachim Breitner
2018-05-16[sphinx] Bump timeout. Closes #7532.Clément Pit-Claudel
2018-05-16[sphinx] Fix mistake in index.Théo Zimmermann
2018-05-16[sphinx] Improve rewrite section in tactic chapter.Théo Zimmermann
Including a fix to the example given in #7407.
2018-05-16Merge PR #7079: Remove naked pointers from the VMMaxime Dénès
2018-05-16Merge PR #7391: Add a small documentation writer's guideMaxime Dénès
2018-05-16[windows] Don't make menhir and int anymore.Emilio Jesus Gallego Arias
As pointed out by @MSoegtropIMC [here](https://github.com/coq/coq/pull/7522#issuecomment-389478963) there are not needed to build the packages, so not building them will save a couple of minutes.
2018-05-16unit tests: add .merlinGaëtan Gilbert
2018-05-16add unit tests to test suitePaul Steckler
2018-05-16Merge PR #7436: [travis] Remove some more jobs from PR testing now that they ↵Gaëtan Gilbert
are on Gitlab.
2018-05-16Minor update of the documentation/man about the resource file.Hugo Herbelin
2018-05-16document 7025Enrico Tassi
2018-05-16[ssr] fix after to_constr ~abort_on_undefined_evars was addedEnrico Tassi
2018-05-16Merge PR #7484: Fix non-portable shebang in test-suite.Enrico Tassi
2018-05-16Merge PR #7227: [ssr] import ssreflect test suite from math-compMaxime Dénès
2018-05-16Merge PR #7442: Gitlab: build docker image in pipeline and use through registry.Emilio Jesus Gallego Arias
2018-05-16[ci] Don't build lite versions of CI developments.Emilio Jesus Gallego Arias
In the original Travis CI setup, the per-job time limit was an issue. However, Gitlab has much improved this problem due to a) Coq not being built for each contrib, b) user-configurable time limit. We thus disable the expensive builds from Travis: `fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`, `math-comp`, `unimath`, `vst` and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`] in full. We also update the `math-comp` script as the `odd-order` theorem lives in a separate repository and it is a key CI case.
2018-05-16[travis] Remove some more jobs from PR testing now that they are on Gitlab.Emilio Jesus Gallego Arias
This is a "test" PR, but could be merged if we like it.
2018-05-16[ide] Don't set `quiet` on start.Emilio Jesus Gallego Arias
This makes `coqidetop` behavior consistent with the one of `coqtop`. This was likely needed in the past when Coq used to print all kind of stuff to stdout, including goal display. Now, it is not the case anymore and this flag mainly controls printing verbosity.
2018-05-16Merge PR #7507: gitlab CI: fix [warnings] templateEmilio Jesus Gallego Arias
2018-05-16Merge PR #7505: Pick up user overlays when running GitLab CI on PRs.Emilio Jesus Gallego Arias
2018-05-15Merge PR #7519: git / gpg integration linkThéo Zimmermann
2018-05-15Merge PR #7465: Don't use ref universe_opt_subst in universe normalisation ↵Pierre-Marie Pédrot
function
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 01:52:16 +0000