aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-01-09Merge PR #9322: [ci] Update fiat-crypto legacyGaëtan Gilbert
2019-01-09Merge PR #9316: Fix #3934: coqc -time -quick gives unreadable outputEnrico Tassi
2019-01-09Merge PR #9273: Fix #9272: `Unset Nested Proofs Allowed` does not capture ↵Enrico Tassi
nested `Ins…
2019-01-08[ci] Update fiat-crypto legacyJason Gross
Once https://github.com/mit-plv/fiat-crypto/pull/477 is merged, the master branch will no longer contain the files nor the targets for fiat-crypto legacy. (We should perhaps consider moving fiat-crypto legacy to coq-community as a source of vm and printing tests.)
2019-01-08Fix #3934: coqc -time -quick gives unreadable outputMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` ↵Maxime Dénès
proofs. We forbid commands that may open proofs inside proofs.
2019-01-08Merge PR #9282: [ssrmatching] update license banner (fix #9281)Maxime Dénès
2019-01-08Merge PR #9292: Fixing some wrong scopes of variables in the interpretation ↵Emilio Jesus Gallego Arias
of the "in" clause of a "match"
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-07Merge PR #8373: Fixes #8369: Not_found in printing message about an ↵Matthieu Sozeau
unresolved subevar.
2019-01-07Merge PR #9309: [ci] Add Verdi Raft with dependencies to CIEmilio Jesus Gallego Arias
2019-01-06Merge PR #9305: Remove formal-topology from CIGaëtan Gilbert
2019-01-06Merge PR #8977: Update .mailmap.Gaëtan Gilbert
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
This is a reworking of 7fd28dc9: instead of using words such as "domain of", "codomain of" to refer to a position in the instance of the original evar, we simply display the instance and the name of the unresolved evar in this instance. This is both simpler and more informative. (The positional words remain useful for printing the evar_map in debugging though.) In passing, this fixes #8369 (Not_found in printing message about an unresolved subevar). Incidentally add possible breaking while printing "in environment".
2019-01-05[ci] Add Verdi Raft with dependencies to CIKarl Palmskog
2019-01-04Merge PR #9264: Fix shallow flag in vernac statePierre-Marie Pédrot
2019-01-04Remove formal-topology from CIMaxime Dénès
This was suggested by the author. See https://github.com/bmsherman/topology/issues/23
2019-01-02Merge PR #9276: Remove dead code from CClosure.Maxime Dénès
2018-12-30Fixing an interpretation bug of the "in" clause of "match".Hugo Herbelin
- The head of "in" was wrongly considered binding - Aliases in the "in" pattern were not taken into account
2018-12-30Mini-reorganization of functions about cases pattern reducing to a variable.Hugo Herbelin
2018-12-27Merge PR #9277: [dune] Build refman with fatal warnings like in the Makefile ↵Emilio Jesus Gallego Arias
build.
2018-12-27Merge PR #9224: Move lint job to gitlabEmilio Jesus Gallego Arias
2018-12-26[dune] Build refman with fatal warnings by default like in the Makefile build.Théo Zimmermann
The way to override this default is not exactly the same as in the legacy Makefile but it has been documented as well.
2018-12-26Merge PR #8734: Make diffs work for more input stringsHugo Herbelin
2018-12-25Merge PR #9249: Fixing printing bug due to using equality wrongly checking ↵Emilio Jesus Gallego Arias
hash keys of kernel names (or checking wrong hash keys?)
2018-12-25Merge PR #9278: [ci] Annotate plugins and libraries.Emilio Jesus Gallego Arias
2018-12-25Fixing printing bug due to using equality ill-checking hash key of kernel name.Hugo Herbelin
Thanks to Georges Gonthier for noticing it. Expanding a few Pervasives.compare at this occasion.
2018-12-25Adding a comparison combinator for pairs.Hugo Herbelin
2018-12-25[ssrmatching] update license banner (fix #9281)Enrico Tassi
This commit fixes a leftover of the merge of ssrmatching where the .ml code received the appropriate banner, while the .v and .mli di dnot.
2018-12-23[ci] Annotate plugins and libraries.Théo Zimmermann
This will allow @coqbot to automatically add appropriate needs labels (overlay or fixing) depending on whether it breaks a plugin or a library.
2018-12-23Remove dead code from CClosure.Pierre-Marie Pédrot
It seems that it was a remnant of a time where Reductionops would share the same data types.
2018-12-23Merge PR #9243: Fix line ending issues (azure related)Michael Soegtrop
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-21Merge PR #9247: Fix typo in gallina specification language docThéo Zimmermann
2018-12-21Merge PR #9266: Make @SkySkimmer an owner of test-suite/report.shThéo Zimmermann
2018-12-21Move lint job to gitlabGaëtan Gilbert
This changes the semantics a bit since we don't have TRAVIS_COMMIT_RANGE anymore, instead we do per-commit linting for the commits since the last merge commit.
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-21Merge PR #9265: Do not exclude "opened" bugs from reportGaëtan Gilbert
2018-12-21Merge PR #9183: List members of the code of conduct enforcement team.Matthieu Sozeau
2018-12-21Make @SkySkimmer an owner of test-suite/report.shMaxime Dénès
2018-12-21Do not exclude "opened" bugs from reportMaxime Dénès
2018-12-21Fix shallow flag in vernac stateMaxime Dénès
Was incorrect due to a leftover in #9220.
2018-12-21Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.Maxime Dénès
2018-12-20Make diffs work for more input stringsJim Fehrle
Diff code uses the lexer to recognize tokens in the inputs, which can be Pp.t's or strings. To add the highlights in the Pp.t, the diff code matches characters in the input to characters in the tokens. Current code fails for inputs containing quote marks or "(*" because the quote marks and comments don't appear in the tokens. This commit adds a "diff mode" to the lexer to return those characters, making the diff routine more robust.
2018-12-20Merge PR #8488: Warning when using automatic template polymorphismPierre-Marie Pédrot
2018-12-20Fix line ending issuesGaëtan Gilbert
Try to mimick MSoegtropIMC (https://github.com/coq/coq/pull/9243#issuecomment-448968353 )
2018-12-20Merge PR #9200: [ssr] make `>` stand aloneMaxime Dénès
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
(in case of side effects) Also: Fix #4781 Fix #4496
2018-12-19Add CHANGES for auto-template warning.Gaëtan Gilbert
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:50:40 +0000