| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |||
| 2019-02-18 | [gitlab] [docker] [ci] Remove "edge" compiler switch. | Emilio Jesus Gallego Arias | |
| Since a long time the compiler switch is not very useful as it is not used to test any CI. The `edge+flambda` version seems stable enough to carry out the `edge` testing by itself, thus we remove the `egde` switch saving valuable Docker image size and Gitlab runners. We also tweak the `pkg:opam` job as to correctly set the version of the pinned local package. | |||
| 2019-02-17 | Separate variance and universe fields in inductives. | Gaëtan Gilbert | |
| I think the usage looks cleaner this way. | |||
| 2019-02-12 | [tactics] Remove dependency of abstract on global proof state. | Emilio Jesus Gallego Arias | |
| In order to do so we place the polymorphic status and name in the read-only part of the monad. Note the added comments, as well as the fact that almost no part of tactics depends on `proofs` nor `interp`, thus they should be placed just after pretyping. Gaëtan Gilbert noted that ideally, abstract should not depend on the polymorphic status, should we be able to defer closing of the constant, however this will require significant effort. Also, we may deprecate nameless abstract, thus rending both of the changes this PR need unnecessary. | |||
| 2019-02-11 | Merge PR #9465: [Nix-CI] Add iris and lambda-rust | Maxime Dénès | |
| Reviewed-by: maximedenes | |||
| 2019-02-09 | remove VERBOSE=1, gitlab log shows that `-async-proofs-tac-j 1` was indeed ↵ | Samuel Gruetter | |
| passed https://gitlab.com/coq/coq/-/jobs/158737429 | |||
| 2019-02-08 | Workaround for CI not having enough RAM for bedrock2: `-async-proofs-tac-j 1` | Samuel Gruetter | |
| COQMF_ARGS is a bedrock2-specific name to pass extra arguments to coq_makefile, and we use VERBOSE=1 for better debuggability | |||
| 2019-02-08 | Update overlay file | Matthieu Sozeau | |
| 2019-02-08 | Add overlay for Equations | Matthieu Sozeau | |
| 2019-02-08 | Add overlays for unicoq and mtac2 | Matthieu Sozeau | |
| 2019-02-05 | [Nix-CI] Add lambda-rust | Vincent Laporte | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |