| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-01-11 | Merge pull request #8778 from SkySkimmer/merge-plugin-tuto | Yves Bertot | |
| Move plugin tutorial to Coq repo | |||
| 2019-01-08 | [ci] Update fiat-crypto legacy | Jason 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-08 | Integrate plugin tutorial after code import | Gaëtan Gilbert | |
| 2019-01-07 | Merge PR #9309: [ci] Add Verdi Raft with dependencies to CI | Emilio Jesus Gallego Arias | |
| 2019-01-05 | [ci] Add Verdi Raft with dependencies to CI | Karl Palmskog | |
| 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 | |||
| 2018-12-27 | Merge PR #9224: Move lint job to gitlab | Emilio Jesus Gallego Arias | |
| 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-20 | Fix line ending issues | Gaëtan Gilbert | |
| Try to mimick MSoegtropIMC (https://github.com/coq/coq/pull/9243#issuecomment-448968353 ) | |||
| 2018-12-18 | Merge PR #9215: Set up CI with Azure Pipelines | Emilio Jesus Gallego Arias | |
| 2018-12-17 | Merge PR #9153: [api] Move reduction modules to `tactics` | Pierre-Marie Pédrot | |
| 2018-12-17 | Set up CI with Azure Pipelines | Gaëtan Gilbert | |
| 2018-12-17 | Merge PR #8856: [gitlab] Test Ocaml trunk. | Gaëtan Gilbert | |
| 2018-12-17 | Fix git line ending conversion in windows | Gaëtan Gilbert | |
| 2018-12-17 | Merge PR #9220: Move shallow state logic to the function preparing state for ↵ | Enrico Tassi | |
| workers | |||
| 2018-12-16 | Merge PR #9172: [proof] Rework proof interface. | Pierre-Marie Pédrot | |
| 2018-12-14 | [dune] [gitlab] Test OCaml trunk. | Emilio Jesus Gallego Arias | |
| We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too. | |||
| 2018-12-14 | Merge PR #9147: [dune] [doc] Support for building the reference manual with ↵ | Théo Zimmermann | |
| Dune. | |||
| 2018-12-14 | [proof] Rework proof interface. | Emilio Jesus Gallego Arias | |
| - deprecate the old 5-tuple accessor in favor of a view record, - move `name` and `kind` proof data from `Proof_global` to `Proof`, this will prove useful in subsequent functionalizations of the interface, in particular this is what abstract, which lives in the monads, needs in order no to access global state. - Note that `Proof.t` and `Proof_global.t` are redundant anyways. | |||
| 2018-12-13 | Add overlay | Maxime Dénès | |
| 2018-12-13 | Merge PR #9210: Fix issue #9176 : Windows: change cygwin repo | Théo Zimmermann | |
| 2018-12-13 | [dune] [doc] Support for building the reference manual with Dune. | Emilio Jesus Gallego Arias | |
| This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted. | |||
| 2018-12-13 | Merge PR #9217: [ci] [appveyor] Temporally disable test suite on Appveyor. | Gaëtan Gilbert | |
| 2018-12-13 | [ci] [appveyor] Temporally disable test suite on Appveyor. | Emilio Jesus Gallego Arias | |
| Hopefully we will re-enable it back soon, I am preparing a refactoring that should make it more robust w.r.t paths and changes on Windows which will enable to use a faster build system. But now it is timing out 100% of the times [due to #8655] so it is not useful. | |||
| 2018-12-12 | Higher-level libobject API for objects with fixed scopes | Maxime Dénès | |
| 2018-12-12 | Fix issue #9176 : Windows: change cygwin repo | Michael Soegtrop | |
| 2018-12-12 | Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix ↵ | Maxime Dénès | |
| comments. | |||
| 2018-12-11 | Fixing imports in debug printers: gramlib depends on Loc which is in lib.cma. | Hugo Herbelin | |
| 2018-12-11 | [ci] Clean overlay folder. | Emilio Jesus Gallego Arias | |
| 2018-12-10 | Merge PR #9077: Rename generated directory gramlib__pack -> gramlib/.pack | Emilio Jesus Gallego Arias | |
| 2018-12-09 | fix copy-paste error in CI_ARCHIVEURL | Christian Doczkal | |
| 2018-12-09 | add relation-algebra to CI test suite | Christian Doczkal | |
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-06 | Rename generated directory gramlib__pack -> gramlib/.pack | Gaëtan Gilbert | |
| It's a bit cleaner this way, especially wrt the number of toplevel directories. Also fix warning about undefined GRAMMARCMA while we're at it. | |||
| 2018-12-05 | [ci] Add four color theorem proof to CI | Emilio Jesus Gallego Arias | |
| 2018-12-05 | Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Pierre-Marie Pédrot | |
| 2018-12-05 | Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks. | Pierre-Marie Pédrot | |
| 2018-12-04 | CI: track dev branch of coq-simple-io | Yishuai Li | |
| 2018-12-04 | Merge PR #8187: Notation printing based on scopes (take 2, including bug fixes) | Emilio Jesus Gallego Arias | |
| 2018-12-04 | Merge PR #9053: Document code owner team creation. | Maxime Dénès | |
| 2018-12-04 | Addressing issues with PR#873: performance and use of abbreviation for printing. | Hugo Herbelin | |
| We do a couple of changes: - Splitting notation keys into more categories to make table smaller. This should (a priori) make printing faster (see #6416). - Abbreviations are treated for printing like single notations: they are pushed to the scope stack, so that in a situation such as Open Scope foo_scope. Notation foo := term. Open Scope bar_scope. one looks for notations first in scope bar_scope, then try to use foo, they try for notations in scope foo_scope. - We seize the opportunity of this commit to simplify availability_of_notation which is now integrated to uninterp_notation and which does not have to be called explicitly anymore. | |||
| 2018-12-03 | Merge PR #9112: [release doc] vX.X branches are now automatically protected. | Maxime Dénès | |
| 2018-11-30 | [vernac] [hooks] Refactor towards optional hooks. | Emilio Jesus Gallego Arias | |
| We make `declaration_hook`s optional arguments everywhere, and thus we avoid some "fake" functions having to be passed. This identifies positively the code really using hooks [funind, rewrite, coercions, program, and canonicals] and helps moving toward some hope of reification. | |||
| 2018-11-30 | [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Emilio Jesus Gallego Arias | |
| The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option` | |||
| 2018-11-30 | Merge PR #9102: [ltac] Remove aliases already present in the lower layers. | Pierre-Marie Pédrot | |
| 2018-11-29 | [release doc] vX.X branches are now automatically protected. | Théo Zimmermann | |
| 2018-11-29 | Merge PR #9054: [ci] [appveyor] Move Appveyor to OPAM 2. | Maxime Dénès | |
| 2018-11-28 | [Windows CI] Do not build any addon if WINDOWS is not enabled_all_addons. | Théo Zimmermann | |
| Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com> | |||
| 2018-11-28 | [ltac] Remove aliases already present in the lower layers. | Emilio Jesus Gallego Arias | |
| We remove a few aliases present in the lower layers [`Genintern/Tactypes`] from `Tacexpr`. IMHO this enlarges the API for no good purpose, and difficults analysis. | |||
| 2018-11-27 | [ci] [appveyor] Move Appveyor to OPAM 2. | Emilio Jesus Gallego Arias | |
| We update the Appveyor configuration so it uses OPAM 2.0, and thus it can install newer packages. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |