aac-tactics
aac-tactics copied to clipboard
coq-community
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
The terms are of type `Internal.T env_sym`, so invoking `vm_compute in` on them ends up strongly normalizing the function `env_sym`, which explodes. By using `eval vm_compute` instead, only the bodies...
The ocaml-function Coq.retype (and Coq.tclRETYPE in #34 ) are used at various points. This has to do with the plugin building coq-terms without updating universe constrains (I guess?). This seems...
I recently found this library and found it to be very useful and wish I knew about it years ago. Is it possible/easy to implement `aac_congruence` using the machinery defined...
Adapt to https://github.com/coq/coq/pull/19530 This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the...
Metadata
Owner
Metadata
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]