aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays
AgeCommit message (Collapse)Author
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
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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 00:24:19 +0000