| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-14 | Merge PR #8893: Moving evars_of_term from constr to econstr | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-05-14 | Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2 | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: ppedrot | |||
| 2019-05-14 | Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variables | Pierre-Marie Pédrot | |
| Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-05-14 | Overlay for value-returning run_tactic | Gaëtan Gilbert | |
| 2019-05-13 | Adding overlay for Equations. | Hugo Herbelin | |
| 2019-05-13 | Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵ | Enrico Tassi | |
| prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl | |||
| 2019-05-13 | Add overlay for Unicoq | Maxime Dénès | |
| 2019-05-11 | Merge PR #10052: Cleanup the hypothesis conversion function | Hugo Herbelin | |
| Reviewed-by: herbelin | |||
| 2019-05-10 | Add overlay for elpi | Vincent Laporte | |
| 2019-05-10 | Merge PR #9854: Improve field_simplify on fractions with constant denominator | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: amahboubi Reviewed-by: vbgl | |||
| 2019-05-10 | Add overlays for coq/coq#10052. | Pierre-Marie Pédrot | |
| 2019-05-10 | Merge PR #10120: Clean-up: remove dead appveyor.sh file. | Emilio Jesus Gallego Arias | |
| 2019-05-09 | Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repo | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC | |||
| 2019-05-09 | Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlab | Michael Soegtrop | |
| 2019-05-08 | Remove ltac2 add-on from Windows installer now that it is in the main Coq ↵ | Théo Zimmermann | |
| package. | |||
| 2019-05-08 | Clean-up: remove dead appveyor.sh file. | Théo Zimmermann | |
| 2019-05-07 | Remove overlays for CompCert and VST | Vincent Laporte | |
| 2019-05-07 | [nix-ci] Add coquelicot, improve flocq | Vincent Laporte | |
| 2019-05-07 | Add overlays for CompCert, VST, and coquelicot | Vincent Laporte | |
| 2019-05-07 | Remove ppedrot/ltac2 from CI after integration in main repo | Gaëtan Gilbert | |
| 2019-05-07 | Add overlays. | Pierre-Marie Pédrot | |
| 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 | |||
