| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-01-19 | Merge PR #11214: Add a script to pin CI developments. | Gaëtan Gilbert | |
| Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2020-01-19 | Merge PR #11368: Turn trailing implicit warning into an error | Hugo Herbelin | |
| Ack-by: Zimmi48 Reviewed-by: herbelin Ack-by: maximedenes | |||
| 2020-01-19 | Merge PR #11398: Fix issue #11396 : Rlist hides standard list constructors ↵ | Pierre-Marie Pédrot | |
| cons and nil Reviewed-by: Zimmi48 Reviewed-by: herbelin Reviewed-by: ppedrot | |||
| 2020-01-19 | Removing text saying XML is future of PG, adding explicitly vscoq as a user | Hugo Herbelin | |
| 2020-01-17 | Fix issue #11396 : Rlist hides standard list constructors cons and nil | Michael Soegtrop | |
| 2020-01-15 | [Nix] Update reference to nixpkgs | Vincent Laporte | |
| This brings dune at version 2.1.2 | |||
| 2020-01-15 | [Nix/CI] Add verdi-raft | Vincent Laporte | |
| 2020-01-15 | [Nix/CI] Update fiat_crypto | Vincent Laporte | |
| 2020-01-09 | Merge PR #11371: [merge script] Never bypass outdated branch sanity check. | Jason Gross | |
| Reviewed-by: JasonGross | |||
| 2020-01-08 | let CI test bedrock2's 'tested' branch instead of 'master' | Samuel Gruetter | |
| 2020-01-07 | [merge script] Never bypass outdated branch sanity check. | Théo Zimmermann | |
| The message was confusing and the prompt let one reviewer think the merge script would take care of doing the pull, which it doesn't. | |||
| 2020-01-07 | Trailing implicit error: overlays | SimonBoulier | |
| 2020-01-03 | Merge PR #11295: Use code owner teams for every component. | Maxime Dénès | |
| Reviewed-by: maximedenes | |||
| 2019-12-31 | Merge PR #11338: Remove uses of Global in Evd API. | Gaëtan Gilbert | |
| Reviewed-by: ejgallego Reviewed-by: herbelin | |||
| 2019-12-28 | Merge PR #11323: Fix mulc on 32-bit architectures | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC | |||
| 2019-12-27 | Add critical-bugs entry, tests-suite file, and code comment. | Guillaume Melquiond | |
| 2019-12-26 | Remove uses of Global in Evd API. | Pierre-Marie Pédrot | |
| Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional environment instead of querying the imperative global one. We percolate this change as higher up as possible. | |||
| 2019-12-24 | Update merging doc following the full move to teams. | Théo Zimmermann | |
| Integrate merging doc in the main contributing document. | |||
| 2019-12-24 | Merge PR #11316: Windows: switch OCaml to 4.08.1 | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-12-23 | Windows: switch OCaml to 4.08.1 | Michael Soegtrop | |
| - remove manual flexlink circular dependency handling - use standard configure process instead of hand made windows make files - enable parallel build - remove bootstrapping step (maybe should be there for release builds) | |||
| 2019-12-22 | Rename files with Class in their name to make their role clearer. | Pierre-Marie Pédrot | |
| We restrict to those that are actually related to typeclasses, and perform the following renamings: Classops --> Coercionops Class --> ComCoercion | |||
| 2019-12-18 | Merge PR #9786: Fix Equation's ci script | Pierre-Marie Pédrot | |
| Reviewed-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-12-16 | Overlay for #11027 | Gaëtan Gilbert | |
| 2019-12-13 | Merge PR #11259: [make] Rename Makefile to Makefile.make and INSTALL to ↵ | Théo Zimmermann | |
| INSTALL.md Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: jfehrle | |||
| 2019-12-13 | Add ocamlformat dependency to Nix file | Maxime Dénès | |
| 2019-12-13 | [doc] [INSTALL] split make-based install instructions to its own file. | Emilio Jesus Gallego Arias | |
| 2019-12-13 | [doc] [INSTALL] Port INSTALL to markdown format. | Emilio Jesus Gallego Arias | |
| 2019-12-13 | [fmt] [dune] Add ocamlformat configuration. | Emilio Jesus Gallego Arias | |
| For now we don't enable it in any source file, neither on dune files. `lint-repository` has been updated so it will check `dune build @fmt` returns 0. | |||
| 2019-12-13 | [ci] [docker] Install ocamlformat in docker images. | Emilio Jesus Gallego Arias | |
| 2019-12-13 | Fix Equation's ci script | Matthieu Sozeau | |
| 2019-12-06 | Adding overlay for Quickchick PR#145. | Hugo Herbelin | |
| 2019-12-06 | Moving the diversity of constr printers to a label style. | Hugo Herbelin | |
| This allows to give access to all printing options (e.g. a scope or being-in-context) to every printer w/o increasing the numbers of functions. | |||
| 2019-12-06 | Merge PR #11174: [dune] Update to dune language version 2.0 | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-12-04 | Overlay for ELPI | Hugo Herbelin | |
| 2019-12-04 | [dune] Update to dune language version 2.0 | Emilio Jesus Gallego Arias | |
| This is the minimal set of changes requires for Coq to build under 2.0 mode. We may likely take advantage of some more new features. Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune in older versions as it will install a secondary compiler. | |||
| 2019-12-02 | Remove deprecated compat modifier of Notation / Infix commands. | Théo Zimmermann | |
| And simplify a lot the compatibility infrastructure following this. Update dev/tools/update-compat.py Remove much complexity. Co-authored-by: Jason Gross <jgross@mit.edu> | |||
| 2019-12-02 | [ci] [sf] Add authentication to artifact download. | Emilio Jesus Gallego Arias | |
| It seems we need to pass the token to the actual artifact download. | |||
| 2019-12-02 | [CI] Test latest artifacts of SF instead of the stable version | Maxime Dénès | |
| 2019-12-02 | Add a script to pin CI developments. | Pierre-Marie Pédrot | |
| It is useful for the release process, and there is no reason for somebody to lose time reimplementing it again. | |||
| 2019-11-29 | Merge PR #10931: Add types of changes to changelog entries. | Emilio Jesus Gallego Arias | |
| Ack-by: SkySkimmer Reviewed-by: ejgallego | |||
| 2019-11-28 | Update README and make-changelog tool following introduction of changelog types. | Théo Zimmermann | |
| 2019-11-27 | [ci] Split out the dependencies of fiat-crypto | Jason Gross | |
| 2019-11-27 | [ci] Build slightly more in the fiat-crypto target | Jason Gross | |
| This adds a couple extra files, but not many. | |||
| 2019-11-27 | [release] Update files for 8.12 release per release process. | Emilio Jesus Gallego Arias | |
| 2019-11-26 | Fix #11039: proof of False with template poly and nonlinear universes | Gaëtan Gilbert | |
| Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504. | |||
| 2019-11-25 | Error fatally if update-compat.py gets no flag | Jason Gross | |
| c.f. https://github.com/coq/coq/pull/11032#issue-335944369 Also, change the default from python2 to python3 for update-compat while we're at it, and update file unicode handling accordingly. (Note that this file still works with both python2 and python3.) | |||
| 2019-11-21 | Merge PR #11154: add tlc to ci; please proof read very carefully and test. ↵ | Emilio Jesus Gallego Arias | |
| thanks Reviewed-by: SkySkimmer Reviewed-by: ejgallego | |||
| 2019-11-21 | [coq] Untabify the whole ML codebase. | Emilio Jesus Gallego Arias | |
| We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` | |||
| 2019-11-21 | add tlc to ci; please proof read very carefully and test. thanks | charguer | |
| 2019-11-12 | Printing name of change log file in changelog script. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |