aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays
AgeCommit message (Collapse)Author
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-01Overlays for UIP in SPropGaëtan Gilbert
2020-06-29Adding overlay.Pierre-Marie Pédrot
2020-06-26[ci] Add overlays for PR #12372Emilio Jesus Gallego Arias
2020-06-19Add overlays.Pierre-Marie Pédrot
2020-05-18[ci] Old overlay cleanup.Emilio Jesus Gallego Arias
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
2020-05-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-15Add overlays for coqhammer and coq-dpdgraph.Hugo Herbelin
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
Re-raising inside exception handlers must be done with care in order to preserve backtraces; even if newer OCaml versions do a better job in automatically spilling `%reraise` in places that matter, there is no guarantee for that to happen. I've done a best-effort pass of places that were re-raising incorrectly, hopefully I got the logic right. There is the special case of `Nametab.error_global_not_found` which is raised many times in response to a `Not_found` error; IMHO this error should be converted to something more specific, however the scope of that change would be huge as to do easily...
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares
2020-05-13Overlay elpiHugo Herbelin
2020-05-10Add overlays.Pierre-Marie Pédrot
2020-05-09Add overlaysPierre Roux
2020-05-07[ci] overlay for coq-elpiEnrico Tassi
2020-05-03Add overlays.Pierre-Marie Pédrot
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-21Overlay for fiat-crypto, Mtac2, MetaCoq and UniMath.Hugo Herbelin
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode.
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-13Overlay for partial importsGaëtan Gilbert
2020-04-06Add overlays.Pierre-Marie Pédrot
2020-03-30[ci] [overlays] Adapt to declare API changes.Emilio Jesus Gallego Arias
- problem with metacoq overlay ; it expects to send a non-ground constant to the kernel, now it fails at prepare. Record Sigma (A : Type) (B : A -> Type) : Type := { fst : A ; snd : B fst }. Arguments fst {A B}. Arguments snd {A B}. Quote Recursively Definition foo := (fst, snd). There is a hack on the overlay, we need to discuss it a bit more.
2020-03-22Overlay for QuickChickHugo Herbelin
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
There is a lot of check overhead in the code, we will try to provide a more convenient API for manipulation of remaining obligations.
2020-03-19[ci] Overlays for declare interface refactoring.Emilio Jesus Gallego Arias
2020-03-18Adding overlays.Pierre-Marie Pédrot
2020-03-16[ci] Cleanup old overlays.Emilio Jesus Gallego Arias
2020-03-09Add CI overlays.Pierre-Marie Pédrot
2020-03-04Add overlay for equations.Hugo Herbelin
2020-03-01[ci] [docker] overlay for elpi 1.10Enrico Tassi
2020-02-19Overlays for Equations, QuickChick and Iris.Hugo Herbelin
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: mattam82
2020-02-14Overlay for Inductive.type_of_inductive doesn't take an envGaëtan Gilbert
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-02-12overlay for removal of optnameGaëtan Gilbert
2020-02-11Add paramcoq overlayMaxime Dénès
2020-02-04Apply suggestions from HugoSimonBoulier
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
2020-02-04Non maximal implicits: add overlays for several librariesSimonBoulier
2020-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
It was virtually unused except in ssr, and there is no reason to clutter the kernel with irrelevant code. Fixes #9390: What is the purpose of the function "kind_of_type"?
2020-01-07Trailing implicit error: overlaysSimonBoulier
2019-12-26Remove 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-22Rename 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-16Overlay for #11027Gaëtan Gilbert
2019-12-06Adding overlay for Quickchick PR#145.Hugo Herbelin
2019-12-04Overlay for ELPIHugo Herbelin
2019-11-05overlayEnrico Tassi
2019-11-01Add overlaysPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 23:37:41 +0000