aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays
AgeCommit message (Collapse)Author
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
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-25[funind] Remove duplicate save function.Emilio Jesus Gallego Arias
AFAICT the reasoning for introducing this function doesn't hold anymore. This is needed for future refactorings that should make some types private.
2019-10-04overlays for sprop default onGaëtan Gilbert
2019-09-18[declaremods] Remove abstraction layer over module interpretation.Emilio Jesus Gallego Arias
Now that we place imperative module declaration on top of module interpretation we can remove the abstraction layer used in `Declaremods`, so the `interp_modast` parameter goes away. Improvement suggested by Gaëtan Gilbert.
2019-09-17Merge PR #10738: update elpi to 1.7Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-09-17Overlay for VSTMaxime Dénès
2019-09-16Add SF overlayMaxime Dénès
2019-09-07overlay for elpiEnrico Tassi
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ↵Pierre-Marie Pédrot
proof data on top of declare. Reviewed-by: ppedrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on ↵Emilio Jesus Gallego Arias
top of declare. This PR is a follow up to #10406 , moving the then introduced `proof_entry` type to `Declare`. This makes sense as `Declare` is the main consumer of the entry type, and already provides the constructors for it. This is a step towards making the entry type private, which will allow us to enforce / handle invariants on entry data better. A side-effect of this PR is that now `Proof_global` does depend on `Declare`, not the other way around, but that makes sense given that closing an interactive proof will be a client of declare. Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into tactics due to `abstract`, at some point we may be able to unify all them into a single file in `vernac`.
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
We replace some uses of `raise (UserError ...)` with `CErrors.user_err`, ideally we would like to make the error raising API not depend on the exception themselves, but that's still a long way to go. We also rename the `Timeout` exception as to clarify purpose in the codebase, given that it has 3 different ones as of today. cc: #7560
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function.
2019-08-09Overlay for #10642Gaëtan Gilbert
2019-07-18Adding overlays.Pierre-Marie Pédrot
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-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-17[ci] Overlays for #9645Emilio Jesus Gallego Arias
2019-06-16Overlays for Mtac2 and Equations.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 22:14:29 +0000