| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-01-06 | Fixes #4633: more explicit error message when referring to a generated evar. | Hugo Herbelin | |
| 2019-01-06 | Renaming pr_evar_suggested_name into -> evar_suggested_name. | Hugo Herbelin | |
| Since it returns an Id.t and not a Pp.t. | |||
| 2019-01-05 | [ci] Add Verdi Raft with dependencies to CI | Karl Palmskog | |
| 2019-01-05 | Remove outdated gitignore coqprojectfile.ml | Gaëtan Gilbert | |
| 2019-01-04 | Handle local definitions in implicit arguments of Instance | Jasper Hugunin | |
| 2019-01-04 | Merge PR #9264: Fix shallow flag in vernac state | Pierre-Marie Pédrot | |
| 2019-01-04 | Remove formal-topology from CI | Maxime Dénès | |
| This was suggested by the author. See https://github.com/bmsherman/topology/issues/23 | |||
| 2019-01-04 | Default disable auto template warning. | Gaëtan Gilbert | |
| The situation is too unclear to make it of general use, plus it has some issues (#9296) I'm not deleting the warning as it can still be useful to find which types are template for those who want to experiment. | |||
| 2019-01-02 | Merge PR #9276: Remove dead code from CClosure. | Maxime Dénès | |
| 2018-12-30 | Fixing 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-30 | Mini-reorganization of functions about cases pattern reducing to a variable. | Hugo Herbelin | |
| 2018-12-30 | Do not take universes into account in lia reification. | Pierre-Marie Pédrot | |
| This is slightly blunt, it might be the case that we get delayed constraints that cannot be solved resulting in a later universe inconsistency, but it looks highly unlikely on arithmetical statements. Alternatively we would have threaded the unification state, but this would have required a much deeper change. Fixes #9268. | |||
| 2018-12-27 | Merge PR #9277: [dune] Build refman with fatal warnings like in the Makefile ↵ | Emilio Jesus Gallego Arias | |
| build. | |||
| 2018-12-27 | Merge PR #9224: Move lint job to gitlab | Emilio 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-26 | Merge PR #8734: Make diffs work for more input strings | Hugo Herbelin | |
| 2018-12-25 | [windows] Cleanup cruft from `dev/build/windows` | Emilio Jesus Gallego Arias | |
| The amount of cruft we are carrying there is high enough as to even difficult navigation. More cleanup should be performed, but this is a first step. | |||
| 2018-12-25 | Merge 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-25 | Merge PR #9278: [ci] Annotate plugins and libraries. | Emilio Jesus Gallego Arias | |
| 2018-12-25 | Fixing 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-25 | Adding 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-23 | Remove 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-23 | Merge PR #9243: Fix line ending issues (azure related) | Michael Soegtrop | |
| 2018-12-22 | Merge PR #9248: Fix #7904: update proofview env after ltac constr:() | Pierre-Marie Pédrot | |
| 2018-12-21 | Merge PR #9247: Fix typo in gallina specification language doc | Théo Zimmermann | |
| 2018-12-21 | Merge PR #9266: Make @SkySkimmer an owner of test-suite/report.sh | Théo Zimmermann | |
| 2018-12-21 | Move lint job to gitlab | Gaë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-21 | Fix #9240: Register for IDProp causes anomaly when non constant | Gaëtan Gilbert | |
| 2018-12-21 | Merge PR #9265: Do not exclude "opened" bugs from report | Gaëtan Gilbert | |
| 2018-12-21 | Merge PR #9183: List members of the code of conduct enforcement team. | Matthieu Sozeau | |
| 2018-12-21 | Make @SkySkimmer an owner of test-suite/report.sh | Maxime Dénès | |
| 2018-12-21 | Do not exclude "opened" bugs from report | Maxime Dénès | |
| 2018-12-21 | Fix shallow flag in vernac state | Maxime Dénès | |
| Was incorrect due to a leftover in #9220. | |||
| 2018-12-21 | Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print. | Maxime Dénès | |
| 2018-12-20 | Make diffs work for more input strings | Jim 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-20 | Relicense to Unlicense | Gaë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-20 | Merge PR #8488: Warning when using automatic template polymorphism | Pierre-Marie Pédrot | |
| 2018-12-20 | Fix line ending issues | Gaëtan Gilbert | |
| Try to mimick MSoegtropIMC (https://github.com/coq/coq/pull/9243#issuecomment-448968353 ) | |||
| 2018-12-20 | Merge PR #9200: [ssr] make `>` stand alone | Maxime Dénès | |
| 2018-12-19 | Fix #7904: update proofview env after ltac constr:() | Gaëtan Gilbert | |
| (in case of side effects) Also: Fix #4781 Fix #4496 | |||
| 2018-12-19 | Add CHANGES for auto-template warning. | Gaëtan Gilbert | |
| 2018-12-19 | Put #[universes(template)] in outputs tests | Gaëtan Gilbert | |
| 2018-12-19 | Put #[universes(template)] on all auto template spots in stdlib | Gaëtan Gilbert | |
| 2018-12-19 | warn when using auto template, funind never uses template poly | Gaëtan Gilbert | |
| The warning can be avoided with the attributes, (or just disable the warning itself I guess). | |||
| 2018-12-19 | Merge PR #9139: [engine] Allow debug printers to access the environment. | Pierre-Marie Pédrot | |
| 2018-12-19 | Merge PR #9159: Make ugraph implementation abstract wrt universe specifics | Pierre-Marie Pédrot | |
| 2018-12-19 | Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names ↵ | Pierre-Marie Pédrot | |
| in right-hand side | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |