issues
search
mit-plv
/
rewriter
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Other
22
stars
20
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Bump etc/coq-scripts from `e4d9e81` to `4327aa1`
#162
dependabot[bot]
closed
1 week ago
0
Use docker for all Coq versions
#161
JasonGross
closed
2 weeks ago
0
Adapt to coq/coq#19620 (Global.push_context_set no strict argument)
#160
SkySkimmer
closed
6 days ago
3
Adapt to https://github.com/coq/coq/pull/19530
#159
proux01
closed
1 month ago
2
[CI] Update Python to install python-is-python3
#158
JasonGross
closed
2 months ago
0
speedup wf{3,4}_of_wf by factorizing raw matches to definitions
#157
SkySkimmer
closed
2 months ago
2
Adapt to coq/coq#19384 (cleanup ustate universe demote APIs)
#156
SkySkimmer
closed
2 months ago
4
Rely on upstreamed Ltac2 functions (prompted by coq/coq#18973).
#155
rlepigre
closed
4 months ago
1
Bump etc/coq-scripts from `857071d` to `e4d9e81`
#154
dependabot[bot]
closed
5 months ago
0
Schedule dependabot updates leading fiat-crypto
#153
JasonGross
closed
6 months ago
0
Bump etc/coq-scripts from `5876e80` to `857071d`
#152
dependabot[bot]
closed
6 months ago
0
Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01
#151
rtetley
closed
6 months ago
2
Bump etc/coq-scripts from `7b54b75` to `5876e80`
#150
dependabot[bot]
closed
7 months ago
0
Adapt to coq/coq#18624 (Tac2ffi / Tac2val split)
#149
SkySkimmer
closed
8 months ago
1
adapt to coq/coq#18563
#148
andres-erbsen
closed
8 months ago
0
Fix nested unordered lists in README.md
#147
divergentdave
closed
9 months ago
0
Performance debug and optimize `replace_type_try_transport`
#146
JasonGross
opened
10 months ago
0
[CI] [Alpine] Don't use PR version of Alpine Coq
#145
JasonGross
closed
8 months ago
0
More error messages when .coq-version creation fails
#144
JasonGross
closed
10 months ago
0
Add more debug profiling (`replace_type_try_transport`)
#143
JasonGross
closed
10 months ago
0
Move unfolding of `fst` and `snd` earlier
#142
JasonGross
closed
10 months ago
0
Add profiling for cbn
#141
JasonGross
closed
10 months ago
0
[CI] Don't duplicate warnings
#140
JasonGross
closed
10 months ago
0
Bump etc/coq-scripts from `d3dc888` to `7b54b75`
#139
dependabot[bot]
closed
10 months ago
1
Add Alpine CI
#138
JasonGross
closed
10 months ago
0
[CI] docker-coq->coq-docker,describe-system-config
#137
JasonGross
closed
10 months ago
0
[CI] Also test Coq 8.18
#136
JasonGross
closed
10 months ago
0
Allow prove_eq_by_Proper to prove Proper instances recursively and by assumption
#135
JasonGross
closed
10 months ago
0
Provide a convenience hypothesis with eqv assumptions in rewrite rules side-conditions
#134
JasonGross
closed
10 months ago
0
Add expr.reify_as_interp_related
#133
JasonGross
closed
10 months ago
0
More expressive debugging in `handle_reified_rewrite_rules_interp`
#132
JasonGross
closed
10 months ago
0
Fix unfolding of let in rewrite rule proving
#131
JasonGross
closed
10 months ago
0
Allow leaving over shelved goals when debugging cache_term
#130
JasonGross
closed
10 months ago
0
Add `prod_rect_nodep_eta`
#129
JasonGross
closed
10 months ago
0
Add `related_hetero_and_Proper`
#128
JasonGross
closed
10 months ago
0
Add type.eqv_of_is_not_higher_order
#127
JasonGross
closed
10 months ago
0
Generalize is_not_higher_order
#126
JasonGross
closed
10 months ago
0
Add more wf3/wf4 proofs
#125
JasonGross
closed
11 months ago
0
Add expr.Wf4
#124
JasonGross
closed
11 months ago
0
Fix Util/Strings/String.v
#123
Villetaneuse
closed
11 months ago
0
Adapt to coq/coq#18280 (case relevance outside case info)
#122
SkySkimmer
closed
11 months ago
1
Bump etc/coq-scripts from `2df5dbe` to `d3dc888`
#121
dependabot[bot]
closed
11 months ago
0
Adapt to coq/coq#18197 (List and Array fold argument order change)
#120
SkySkimmer
closed
11 months ago
0
Adapt to Coq/Coq#18164
#119
Villetaneuse
closed
1 year ago
2
Bump etc/coq-scripts from `8b66ebe` to `2df5dbe`
#118
dependabot[bot]
closed
1 year ago
1
Bump etc/coq-scripts from `8b66ebe` to `bbe2c4c`
#117
dependabot[bot]
closed
1 year ago
2
Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10
#116
rtetley
closed
1 year ago
1
Adapt to coq/coq#18082 (Ltac2 mutable refs are not values)
#115
SkySkimmer
closed
1 year ago
0
`Proj.equal` has been upstreamed, so use it directly
#114
JasonGross
closed
1 year ago
0
Version Util.Tactics2.{Constr,Proj,DestProj}
#113
JasonGross
closed
1 year ago
0
Next