aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-25[ci] [appveyor] Pass -j2 to Appveyor's build.Emilio Jesus Gallego Arias
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-20Relicense to UnlicenseGaëtan Gilbert
This was agreed during the 2018-12-19 Coq Working Group. See eg https://github.com/coq/coq/pull/8778#issuecomment-448932003 Close #7.
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
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-12-19warn when using auto template, funind never uses template polyGaëtan Gilbert
The warning can be avoided with the attributes, (or just disable the warning itself I guess).
2018-12-19Merge PR #9139: [engine] Allow debug printers to access the environment.Pierre-Marie Pédrot
2018-12-19Merge PR #9159: Make ugraph implementation abstract wrt universe specificsPierre-Marie Pédrot
2018-12-19Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names ↵Pierre-Marie Pédrot
in right-hand side
2018-12-19Merge PR #9237: Add Map.find_optPierre-Marie Pédrot
2018-12-19[doc] typoEnrico Tassi
2018-12-19coqchk: fix check for kelim with functorsGaëtan Gilbert
2018-12-19Fix typo in gallina specification language docyudetamago
2018-12-19Merge PR #9081: [dune] A new Makefile.dune target for each package (coq, ↵Théo Zimmermann
coqide-server and coqide).
2018-12-19[dune] Add targets for Coq individual packages.Emilio Jesus Gallego Arias
2018-12-18Merge PR #9223: Fix universe restriction in delayed mode.Pierre-Marie Pédrot
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18Merge PR #6705: [ssr] extended intro patternsCyril Cohen
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-18[ssr] new test by Arthur CharguéraudEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
This commit implements the following intro patterns: Temporary "=> +" "move=> + stuff" ==== "move=> tmp stuff; move: tmp" It preserves the original name. "=>" can be chained to force generalization as in "move=> + y + => x z" Tactics as views "=> /ltac:(tactic)" Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo". Limited to views on the right of "=>", views that decorate a tactic as move or case are not supported to be tactics. Dependent "=> >H" move=> >H ===== move=> ???? H, with enough ? to name H the first non-dependent assumption (LHS of the first arrow). TC isntances are skipped. Block intro "=> [^ H] [^~ H]" after "case" or "elim" or "elim/v" it introduces in one go all new assumptions coming from the eliminations. The names are picked from the inductive type declaration or the elimination principle "v" in "elim/v" and are appended/prepended the seed "H" The implementation makes crucial use of the goal_with_state feature of the tactic monad. For example + schedules a generalization to be performed at the end of the intro pattern and [^ .. ] reads the name seeds from the state (that is filled in by case and elim).
2018-12-18[arguments] cleanupEnrico Tassi
2018-12-18Merge PR #9218: [STM] Better protection for cur_idEnrico Tassi
2018-12-18Merge PR #9222: Fix classification of Set Default Proof Mode.Enrico Tassi
2018-12-18Add comment to acyclicgraph APIGaëtan Gilbert
2018-12-18Merge PR #9160: Avoid user-given names in automatic introduction of bindersPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 20:07:32 +0000