StructTact
StructTact copied to clipboard
uwplse
Coq utility and tactic library.
Currently, it requires using https://coq.inria.fr/opam/extra-dev which holds some other experimental code I do not want to use. Would it be possible to make it available via the default coq opam...
This is a trick I stole from a Coq-club post. ``` Ltac break_exists := repeat match goal with | [ H: exists (varname: _), _ |- _ ] => let...
Maybe this isn't super useful, but it might be nice for consistency
I dont know what this means, but it was suggested and everybody nodded, so I assume its good.
Same issue as with find_rewrite. Should be made more consistent. This was also the place where people said Tactic Notations would be good. I don't know what that means though.
find_rewrite currently has 4 cases which all have weird idiosyncrasies. Most glaring is the first case with 4 arguments. This should be cleaned up and tested on the verdi codebase