Many things - Githubissues

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

MIT License

51 stars 2 forks source link

Closed randair closed 4 years ago

randair commented 4 years ago

Induction on any term, not just named hypotheses
Weird LetIn case handled by apply-in
Symmetry
Decompile Module doesn't import Morphisms or notations
Decompile Module currently requires given module to already be imported (to remove tag)