search

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
MIT License
51 stars 2 forks source link

patch/as tactic #69

Closed randair closed 4 years ago

randair commented 4 years ago

Patch proof tactic of the form "patch old new as hyp_name", which behaves as the Patch Proof command does but creates a hypothesis instead. Common patch functionality is refactored.

randair commented 4 years ago

Oops I left a typo on 137. Fixed and will make the remaining requested changes.

randair commented 4 years ago

Attached is the output of ./build.sh followed by ./test.sh. output.txt

tlringer commented 4 years ago

OK, tests look good. Let's take a shot at the PR feedback when you're in, and then we can move on to producing tactics.