search

uwplse / PUMPKIN-PATCH

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

PUMPKIN isn't smart enough for patching eliminators of different sorts yet #14

Open tlringer opened 5 years ago

tlringer commented 5 years ago

If one of old or new uses nat_rec and the other uses nat_ind, or something like that, PUMPKIN fails. This is especially bad for optimization.