search

uwplse / PUMPKIN-PATCH

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

Run Preprocess automatically #12

Open tlringer opened 5 years ago

tlringer commented 5 years ago

For simplicity and separation of concerns, we started with these separate, but for PUMPKIN PATCH it makes sense to just always Preprocess before running search.

tlringer commented 5 years ago

Should happen before Optimize too