aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: mattam82
2019-07-18Adding overlays.Pierre-Marie Pédrot
2019-07-16Enable Coquelicot, Flocq, Interval and Gappa in extended/release Windows buildsMichael Soegtrop
2019-07-16Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)Michael Soegtrop
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
The changes are large due to `Pervasives` deprecation: - the `Pervasives` module has been deprecated in favor of `Stdlib`, we have opted for introducing a few wrapping functions in `Util` and just unqualified the rest of occurrences. We avoid the shims as in the previous attempt. - a bug regarding partial application have been fixed. - some formatting functions have been deprecated, but previous versions don't include a replacement, thus the warning has been disabled. We may want to clean up things a bit more, in particular w.r.t. modules once we can move to OCaml 4.07 as the minimum required version. Note that there is a clash between 4.08.0 modules `Option` and `Int` and Coq's ones. It is not clear if we should resolve that clash or not, see PR #10469 for more discussion. On the good side, OCaml 4.08.0 does provide a few interesting functionalities, including nice new warnings useful for devs.
2019-07-06[Dockerfile] update menhir versionGaëtan Gilbert
Compcert needs a new menhir.
2019-07-02[ci] Overlays for #10419Emilio Jesus Gallego Arias
2019-06-28Merge PR #10434: [declare] Fine tuning of Hook type.Pierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2019-06-26[ci] Overlays for #10337Emilio Jesus Gallego Arias
2019-06-26[ci] Overlays for #10434Emilio Jesus Gallego Arias
2019-06-24[ci] Overlays for #10316Emilio Jesus Gallego Arias
2019-06-24Add overlays.Pierre-Marie Pédrot
2019-06-21[ci] overlay for coq-elpiEnrico Tassi
2019-06-21[docker] [ci] Update Elpi to version 1.4.0Enrico Tassi
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and ↵Pierre-Marie Pédrot
obligation ones. Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-06-17Adding overlays.Pierre-Marie Pédrot
2019-06-17Merge PR #10382: Ensuring that regular expression filtering in CI (iris) ↵Gaëtan Gilbert
works on MacOS X Reviewed-by: SkySkimmer
2019-06-17[ci] Overlays for #9645Emilio Jesus Gallego Arias
2019-06-16Ensuring regexp filtering in ci works on MacOS X.Hugo Herbelin
Unfortunately, "+" regular expressions are not supported by default with MacOS X's sed. It is told that it would work with option -E though, but the syntax seems then different.
2019-06-16Overlays for Mtac2 and Equations.Hugo Herbelin
2019-06-13Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLaterEnrico Tassi
Ack-by: ejgallego Reviewed-by: gares
2019-06-12Merge PR #10358: [docker] update elpi to 1.3.1Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-06-11overlayEnrico Tassi
2019-06-11Adding an overlay for Equations.Pierre-Marie Pédrot
2019-06-11Overlays for 10319Gaëtan Gilbert
2019-06-11update elpi to 1.3.1Enrico Tassi
2019-06-10[ci] [fiat-crypto] Enable more targets on Coq CIJason Gross
Closes #10353 May be blocked on #10352
2019-06-09[ci] Overlays for move_termination_routine_outEmilio Jesus Gallego Arias
2019-06-08Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.Hugo Herbelin
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-06-06Remove old overlaysGaëtan Gilbert
I updated the readme example using the most recent overlay with only 1 touched development.
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ↵Gaëtan Gilbert
Type's argument Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-06-04update overlaysEnrico Tassi
2019-06-04Overlays for coq/coq#10050 (proof_global API changes)Gaëtan Gilbert
2019-06-01Adding overlay for elpiHugo Herbelin
2019-05-27Overlay for mind_kelim change (#10133)Gaëtan Gilbert
2019-05-24Adding overlays.Pierre-Marie Pédrot
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ↵Maxime Dénès
vernac Reviewed-by: maximedenes
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: vbgl
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based ↵Hugo Herbelin
generalization + cleanups Reviewed-by: herbelin
2019-05-21Fixing typos - Part 1JPR
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged.
2019-05-21Overlay for definition-not-visible overhaulGaëtan Gilbert
2019-05-21Overlay for removing Instance: !type syntaxGaëtan Gilbert
2019-05-17Overlay for removing Generalized 1st argGaëtan Gilbert
2019-05-17[Nix-ci] Update Unicoq patchVincent Laporte
2019-05-17[Nix-CI] Bignums no longer depends on camlp5Vincent Laporte
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 14:47:15 +0000