issues
search
coq-community
/
aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
https://coq-community.org/aac-tactics
Other
29
stars
21
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
reactivate Nix CI for 8.20
#147
palmskog
closed
1 day ago
0
aac_rewrite sensitive to equation ordering
#146
aa755
closed
1 day ago
3
add tests for try aac_rewrite and try aac_normalise
#145
palmskog
closed
3 days ago
0
`aac_normalize` throws despite `try`
#144
aa755
closed
3 days ago
14
Canonical ordering for aac_normalise tactic in master
#143
palmskog
closed
1 month ago
0
Canonical ordering for aac_normalise tactic
#142
palmskog
closed
1 month ago
0
aac_congruence
#141
aa755
opened
1 month ago
20
[build] Fix use of plugin aliases in findlib loading.
#140
ejgallego
closed
1 month ago
0
Adapt to coq/coq#18938 (EConstr.ERelevance)
#139
SkySkimmer
closed
2 months ago
0
Replace calls to "vm_compute in hyps" by plain calls to vm_compute.
#138
silene
opened
2 months ago
4
Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01
#137
rtetley
closed
3 months ago
0
Some cleanups and fix incorrect evar map passing in aac_reflexivity
#136
SkySkimmer
closed
4 months ago
1
aac tactics don't handle goal selectors properly
#135
MSoegtropIMC
closed
4 months ago
3
Don't use vmcast to convert the reified goal and actual goal
#134
SkySkimmer
closed
4 months ago
10
aac_reflexivity leads to QED blow up in trivial case (just one unit removed)
#133
MSoegtropIMC
closed
4 months ago
7
fix some boilerplate
#132
palmskog
closed
6 months ago
0
Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10
#131
rtetley
closed
9 months ago
0
Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03
#130
MSoegtropIMC
closed
1 year ago
0
fix Coq ML deprecation
#129
palmskog
closed
1 year ago
0
Add back missing Prop instances
#128
palmskog
closed
1 year ago
0
purge compatibility notations like Zplus
#127
palmskog
closed
1 year ago
0
consistent naming scheme for instances
#126
palmskog
closed
1 year ago
0
OCaml code documentation and deployment
#125
palmskog
closed
1 year ago
0
Proper instance for List app is provided by Morphisms
#124
palmskog
closed
1 year ago
0
Transfer general Instances.v lemma to Stdlib
#123
palmskog
closed
1 year ago
3
Pervasives to Stdlib
#122
palmskog
closed
1 year ago
0
Adapt w.r.t. coq/coq#16933.
#121
ppedrot
closed
1 year ago
0
Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09
#120
MSoegtropIMC
closed
1 year ago
0
more consistency in coqdoc comments
#119
palmskog
closed
2 years ago
0
code formatting fixes
#118
palmskog
closed
2 years ago
0
add deployment on push to master of website with coqdoc
#117
palmskog
closed
2 years ago
0
adjust Coq code formatting and coqdoc comments
#116
palmskog
closed
2 years ago
0
Backport master fixes and improvements to 8.15
#115
palmskog
closed
2 years ago
0
re-enable simple Nix CI workflow
#114
palmskog
closed
2 years ago
4
call tclRETYPE for lift_reflexivity
#113
palmskog
closed
2 years ago
1
tentative fix for universe constraint issue with lists
#112
palmskog
closed
2 years ago
0
idiomatic proof scripts, require imports, documentation
#111
palmskog
closed
2 years ago
0
switch from global to export locality for instances
#110
palmskog
closed
2 years ago
0
Add list permutation instances and export and document list instances
#109
palmskog
closed
2 years ago
0
Please pick the version you prefer for Coq 8.15 in Coq Platform 2022.02
#108
MSoegtropIMC
closed
2 years ago
5
Adapt w.r.t. coq/coq#15393.
#107
ppedrot
closed
2 years ago
0
Adapt w.r.t. coq/coq#15327.
#106
ppedrot
closed
2 years ago
0
adapt to coq/coq#15220
#105
gares
closed
2 years ago
0
Remove the V82 compatibility layers.
#104
ppedrot
closed
2 years ago
2
Adapt w.r.t. coq/coq#15159.
#103
ppedrot
closed
2 years ago
0
Adapt w.r.t. coq/coq#15142.
#102
ppedrot
closed
2 years ago
0
Adapt to coq/coq#15147 (removal of Typing.unsafe_type_of)
#101
SkySkimmer
closed
2 years ago
0
Nat max
#100
palmskog
closed
2 years ago
0
adapt to #14736
#99
Alizter
closed
2 years ago
5
refresh nix ci configuration
#98
palmskog
closed
2 years ago
0
Next