| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-23 | Merge PR #14075: New level of abstraction for streams with (non-canonical) ↵ | Pierre-Marie Pédrot | |
| location function Reviewed-by: ppedrot | |||
| 2021-04-23 | Merge PR #13965: [abbreviation] user syntax to set interp scope of argument | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot | |||
| 2021-04-23 | Overlay for elpi. | Hugo Herbelin | |
| 2021-04-21 | Merge PR #13911: Remove the :> type cast? | coqbot-app[bot] | |
| Reviewed-by: mattam82 Ack-by: Zimmi48 | |||
| 2021-04-15 | Merge PR #14111: [ci] update elpi to 1.13.1 | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 Ack-by: SkySkimmer | |||
| 2021-04-14 | Update dev/ci/user-overlays/14111-gares-update-elpi.sh | Enrico Tassi | |
| Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2021-04-14 | overlay file | Enrico Tassi | |
| 2021-04-14 | Overlay for no remote counter | Gaëtan Gilbert | |
| 2021-04-07 | overlay | Enrico Tassi | |
| 2021-03-30 | Remove the :> type cast | Jim Fehrle | |
| 2021-03-26 | [ci] overlay file for #13958 | Enrico Tassi | |
| 2021-03-25 | Merge PR #13852: [vernac] Improve alpha-renaming in record projection types | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-03-09 | Add overlay | Kazuhiko Sakaguchi | |
| 2021-03-06 | [vernac] Improve alpha-renaming in record projection types | Li-yao Xia | |
| 2021-02-27 | Add overlay | Pierre Roux | |
| 2021-02-24 | Overlay for Set Debug | Gaëtan Gilbert | |
| 2021-02-11 | Merge PR #13844: [vernac] pass the loc of the whole command to the interp ↵ | coqbot-app[bot] | |
| function Reviewed-by: ejgallego | |||
| 2021-02-11 | [ci] overlay for elpi | Enrico Tassi | |
| 2021-02-11 | overlay for coq-elpi | Enrico Tassi | |
| 2021-01-19 | Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵ | Pierre-Marie Pédrot | |
| pattern Reviewed-by: ppedrot | |||
| 2021-01-18 | Adding overlay for perennial. | Hugo Herbelin | |
| 2021-01-18 | Support locality attributes for Hint Rewrite (including export) | Gaëtan Gilbert | |
| We deprecate unspecified locality as was done for Hint. Close #13724 | |||
| 2021-01-09 | Merge PR #13299: Remember universe instances of constants in notations | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: herbelin | |||
| 2021-01-04 | Remember universe instances of constants in notations | Jasper Hugunin | |
| 2021-01-04 | Add overlays. | Pierre-Marie Pédrot | |
| 2020-12-21 | Add overlays. | Pierre-Marie Pédrot | |
| 2020-12-13 | Update dev/ci/user-overlays/README.md | Enrico Tassi | |
| Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> | |||
| 2020-12-12 | [ci] update doc for overlays | Enrico Tassi | |
| 2020-12-12 | Merge PR #13603: [ci] function to declare projects | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: RalfJung Ack-by: Zimmi48 | |||
| 2020-12-10 | [ci] remove old overlays so that people don't copy them | Enrico Tassi | |
| 2020-12-10 | [ci] simplify overlay scripts | Enrico Tassi | |
| 2020-12-09 | Adding overlays. | Pierre-Marie Pédrot | |
| 2020-11-26 | Merge PR #13415: Separate interning and pretyping of universes | coqbot-app[bot] | |
| Reviewed-by: mattam82 | |||
| 2020-11-26 | [ci] bump elpi to 1.12.0 | Enrico Tassi | |
| 2020-11-25 | Overlays for #13415 | Gaëtan Gilbert | |
| 2020-11-19 | Add overlays for elpi and unicoq. | Hugo Herbelin | |
| 2020-11-18 | [attributes] Add overlays for #13312 | Emilio Jesus Gallego Arias | |
| 2020-11-17 | Merge PR #12653: Syntax for specifying cumulative inductives | coqbot-app[bot] | |
| Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot | |||
| 2020-11-16 | Overlay for Coq-Equations. | Hugo Herbelin | |
| 2020-11-16 | Overlays for cumulative inductive syntax | Gaëtan Gilbert | |
| 2020-11-13 | [record] [ci] Overlay for elpi | Emilio 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-06 | Merge PR #13139: Clean the constr-as-hint API | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2020-11-05 | Add overlays | Pierre Roux | |
| 2020-11-04 | Add overlays. | Pierre-Marie Pédrot | |
| 2020-10-27 | Merge PR #13075: Introducing the foundations for a name-alias-agnostic API | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: gares Ack-by: ejgallego | |||
| 2020-10-23 | Merge PR #13177: Automatically merge overlays with most recent upstream version | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 | |||
| 2020-10-21 | Add overlays. | Pierre-Marie Pédrot | |
| 2020-10-16 | Overlay for elpi. | Hugo Herbelin | |
| 2020-10-12 | Merge PR #12449: Minimize Prop <= i to i := Set | coqbot-app[bot] | |
| Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares | |||
| 2020-10-12 | Automatically merge overlays with most recent upstream version | Gaëtan Gilbert | |
| This avoids the need to rebase the overlay when nothing has changed. | |||
