| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-04-24 | [coq_makefile] Enforce warn_error for plugins. | Emilio Jesus Gallego Arias | |
| The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974 | |||
| 2019-04-20 | overlay for elpi | Enrico Tassi | |
| 2019-04-20 | update elpi to version 1.2 | Enrico Tassi | |
| 2019-04-16 | [ci] Overlays for coq/coq#9165 | Emilio Jesus Gallego Arias | |
| 2019-04-10 | Overlays for Global removal in pretyper | Maxime Dénès | |
| 2019-04-05 | Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01) | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01 | |||
| 2019-04-04 | [CI] Fix build of math-comp dependencies | Maxime Dénès | |
| We were incorrectly calling the global `install` target even when building only subcomponents of the library. | |||
| 2019-04-02 | Merge PR #8984: Declare initial hint databases in prelude | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Reviewed-by: ppedrot | |||
| 2019-04-02 | Add overlays | Pierre Roux | |
| 2019-04-01 | [CI] Disable Coquelicot on Windows | Vincent Laporte | |
| 2019-04-01 | [CI] Coquelicot: use “master” development version | Vincent Laporte | |
| 2019-04-01 | Merge PR #9870: Minor refactoring in canonical structures | Enrico Tassi | |
| Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-04-01 | Merge PR #9815: Multiple payload types in tokens | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot Ack-by: proux01 | |||
| 2019-04-01 | Merge PR #9871: CI: add mit-pdos/argosy | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-04-01 | Merge PR #9872: Fix timing diff script to support non-utf8 | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego Reviewed-by: jashug | |||
| 2019-03-31 | Add overlay | Pierre Roux | |
| 2019-03-31 | Merge PR #9733: [lexer] keyword protected quotation token for arbitrary text | Pierre-Marie Pédrot | |
| Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot | |||
| 2019-03-31 | Revert "iconv bedrock2 CI output to UTF-8" | Jason Gross | |
| This reverts commit 1eb8b9dc3ff0e464c9cd6c7f12a1c9db4fa57423. This commit is no longer necessary | |||
| 2019-03-31 | CI: add mit-pdos/argosy | Tej Chajed | |
| 2019-03-31 | overlay for ltac2 | Enrico Tassi | |
| 2019-03-30 | Error when [foo.(bar)] is used with nonprojection [bar] | Gaëtan Gilbert | |
| (warn if bar is a nonprimitive projection) | |||
| 2019-03-30 | Overlay for Elpi | Vincent Laporte | |
| 2019-03-28 | Use only lowercase for unimath in CI scripts | Gaëtan Gilbert | |
| Fix #9845 | |||
| 2019-03-27 | [proof_global] [ci] Overlays for removal of imperative state. | Emilio Jesus Gallego Arias | |
| 2019-03-26 | Overlays for HoTT, Ltac2, and UniMath | Vincent Laporte | |
| 2019-03-22 | Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵ | Maxime Dénès | |
| proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes | |||
| 2019-03-20 | Add overlays for printer API changes | Maxime Dénès | |
| 2019-03-19 | Merge PR #9647: [default.nix] Enable parallel build | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2019-03-19 | [coqide] [ci] Update GTK toolchain to lablgtk3 | Emilio Jesus Gallego Arias | |
| - Update Docker images to install compatible version of lablgtk3 - We remove unnecesary variables from configure. - We fix path detection of GTK libs in makefile | |||
| 2019-03-19 | CoqIDE: Adapt configuration to require lablgtk3 and gtksourceview3. | Hugo Herbelin | |
| 2019-03-18 | [nix] Update reference to nixpkgs | Vincent Laporte | |
| 2019-03-18 | [nix] Move nixpkgs.nix into the dev/ directory | Vincent Laporte | |
| 2019-03-18 | [nix-ci] Use “master” versions of “coq-ext-lib” and “simple-io” | Vincent Laporte | |
| 2019-03-18 | [nix-ci] Share the reference to nixpkgs with default.nix | Vincent Laporte | |
| 2019-03-17 | iconv bedrock2 CI output to UTF-8 | Andres Erbsen | |
| The timing diff script dies badly on non-utf8 input (https://github.com/coq/coq/issues/9767). | |||
| 2019-03-16 | Add test-suite to Paramcoq CI | Pierre Roux | |
| 2019-03-14 | Overlays for SProp | Gaëtan Gilbert | |
| 2019-03-12 | Merge PR #9389: Implement a method for manual declaration of implicits. | Emilio Jesus Gallego Arias | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug | |||
| 2019-03-12 | Merge PR #7819: Ho matching occ sel | Enrico Tassi | |
| Ack-by: gares Ack-by: herbelin Ack-by: mattam82 Ack-by: ppedrot | |||
| 2019-03-11 | [ci] [docker] Upgrade odoc to 1.4.0 | Emilio Jesus Gallego Arias | |
| This is routine as for API doc writers to be able to access the newer features. | |||
| 2019-03-06 | Merge PR #9476: Constructor type information uses the expanded form. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: gares | |||
| 2019-03-05 | [CI] Add stdlib2 | Vincent Laporte | |
| 2019-02-28 | Constructor type information uses the expanded form. | Pierre-Marie Pédrot | |
| It used to simply remember the normal form of the type of the constructor. This is somewhat problematic as this is ambiguous in presence of let-bindings. Rather, we store this data in a fully expanded way, relying on rel_contexts. Probably fixes a crapload of bugs with inductive types containing let-bindings, but it seems that not many were reported in the bugtracker. | |||
| 2019-02-28 | Overlays for coq/coq#9389 implicits API cleanup | Gaëtan Gilbert | |
| 2019-02-26 | [default.nix] Enable parallel build | Vincent Laporte | |
| 2019-02-23 | [vernac] Unify declaration hooks. | Emilio Jesus Gallego Arias | |
| Supersedes #8718. | |||
| 2019-02-22 | overlay for Equations | Enrico Tassi | |
| 2019-02-20 | [azure] [ci] Build on Windows using Dune. | Emilio Jesus Gallego Arias | |
| We may want to keep the make-based and Dune job, however the make-based setup is tested by the INRIA workers so it may not be needed. In order for some test to run well, we always run in Dune with an absolute path. The easiest way to get a portable absolute path is to use OCaml itself so we introduce a small executable to do that. While we are at it, we do some cleanup of the test-suite `dune` file, in particular we remove useless comments, set `--no-buffer` so results can be seen in real time, and recognize the `NJOBS` variable as we have moved to a Dune version that supports env vars. | |||
| 2019-02-18 | [ci] Resolve commit corresponding to branch when downloading tarball. | Théo Zimmermann | |
| This ensures that the log will contain the commit hash that we tested. This reuses the method from the Windows build script (we have a number of common functions, it would be interesting to start a bash shared library file). | |||
| 2019-02-18 | Merge PR #9590: [gitlab] [docker] [ci] Remove "edge" compiler switch. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |