+ Collapse intro/revert.+ Pass in custom tactics.

uwplse / PUMPKIN-PATCH

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

MIT License

51 stars 2 forks source link

+ Collapse intro/revert.+ Pass in custom tactics. #83

Closed randair closed 4 years ago

randair commented 4 years ago

Collapse adjacent intros + revert.
Able to pass in custom tactics, ex: Decompile theorem with "auto" "omega".

tlringer commented 4 years ago

Also just as an engineering note, when you have a couple of unrelated changes like this over a couple of weeks, it's better to commit them separately, even just for documentation. :)

tlringer commented 4 years ago

Since it seems this will take a bit, can you separate out the first change, get it merged, and move the decompiler into coq-plugin-lib first? I need to make sure I can get the Repair command in master of DEVOID

tlringer commented 4 years ago

Basic functionality merged into coq-plugin-lib. @randair how is the rest going?

tlringer commented 4 years ago

Per discussion, we are merging moving the decompiler to coq-plugin-lib right now, and the relevant decompiler changes will happen in coq-plugin-lib instead. I will leave this PR open and link to that one when relevant

tlringer commented 4 years ago

Oh I guess reopening a PR isn't a thing you can do. In any case I'll link to the relevant PR here when it exists