aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays
AgeCommit message (Collapse)Author
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵Pierre-Marie Pédrot
pattern Reviewed-by: ppedrot
2021-01-18Adding overlay for perennial.Hugo Herbelin
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04Add overlays.Pierre-Marie Pédrot
2020-12-21Add overlays.Pierre-Marie Pédrot
2020-12-13Update dev/ci/user-overlays/README.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-12[ci] update doc for overlaysEnrico Tassi
2020-12-12Merge PR #13603: [ci] function to declare projectscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: RalfJung Ack-by: Zimmi48
2020-12-10[ci] remove old overlays so that people don't copy themEnrico Tassi
2020-12-10[ci] simplify overlay scriptsEnrico Tassi
2020-12-09Adding overlays.Pierre-Marie Pédrot
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
Reviewed-by: mattam82
2020-11-26[ci] bump elpi to 1.12.0Enrico Tassi
2020-11-25Overlays for #13415Gaëtan Gilbert
2020-11-19Add overlays for elpi and unicoq.Hugo Herbelin
2020-11-18[attributes] Add overlays for #13312Emilio Jesus Gallego Arias
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-16Overlay for Coq-Equations.Hugo Herbelin
2020-11-16Overlays for cumulative inductive syntaxGaëtan Gilbert
2020-11-13[record] [ci] Overlay for elpiEmilio Jesus Gallego Arias
We re-expose `declare_projections` and `declare_structure_entry` as it is needed by coq-elpi. Ideally we would provide a better way in recordops to interact with this, in fact `declare_structure_entry` is just a wrapper around recordops + libobject structure so there is hope it goes away entirely in the future. The need for Elpi to manually call `declare_projections` should actually disappear in future refactorings.
2020-11-06Merge PR #13139: Clean the constr-as-hint APIcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-05Add overlaysPierre Roux
2020-11-04Add overlays.Pierre-Marie Pédrot
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: gares Ack-by: ejgallego
2020-10-23Merge PR #13177: Automatically merge overlays with most recent upstream versioncoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-21Add overlays.Pierre-Marie Pédrot
2020-10-16Overlay for elpi.Hugo Herbelin
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares
2020-10-12Automatically merge overlays with most recent upstream versionGaëtan Gilbert
This avoids the need to rebase the overlay when nothing has changed.
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-10-09overlay for mtac2Enrico Tassi
2020-10-09overlay for minim-prop-tosetGaëtan Gilbert
2020-10-08Add overlays for Coq-Equations, aac-tactics.Hugo Herbelin
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ↵coqbot-app[bot]
a context. Reviewed-by: mattam82
2020-09-22Add overlay for Equations.Hugo Herbelin
2020-09-13Add overlays.Pierre-Marie Pédrot
2020-09-03Add Equations overlayMaxime Dénès
2020-08-31Update update_global_env usageGaëtan Gilbert
- take just a ugraph instead of the whole env - rename to update_sigma_univs - push global env lookup a bit further up - fix vernacinterp call to update all surrounding proofs, not just the top one - flip argument order for nicer partial applications
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-28Adding overlay for coq-elpi.Hugo Herbelin
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
Added user overlay for bignums
2020-08-24Merge PR #12565: Dnets now consider axioms as being opaque for pattern ↵coqbot
recognition. Reviewed-by: mattam82
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
Reviewed-by: herbelin Reviewed-by: maximedenes
2020-08-20Adding overlays.Pierre-Marie Pédrot
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
Try just going with the user-given names, and not worrying about what happens with repeated names or anonymous implicits. (Support for anonymous implicits is due to herbelin in #11098.) This PR should not change behaviour in the absence of repeated names. Since repeated names are already a poorly handled corner case, I would recommend changing binder names to avoid overlap in the case of a change in behavior. Since anonymous implicits and implicits with repeated names can already happen, I think this is unlikely to cause too many new problems, though it might exacerbate existing ones. However, I already had to fix one newly possible anomaly, so I can't be too confident. The most common change in external developments was that an argument no longer gets `0` appended to it, causing the `Arguments` command to complain about renaming. To fix this and keep the old name, one can simply use the `rename` flag as suggested, or switch to the new, un-suffixed name. Closes #6785 Closes #12001 Another step towards checking the standard library with `-mangle-names`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:12:35 +0000