Avoid using admit even in tests

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

42 stars 24 forks source link

Closed tchajed closed 3 years ago

tchajed commented 4 years ago

This ensures that grepping the source for admits comes back clean.

samuelgruetter commented 3 years ago

I'm fine with this, just requesting @andres-erbsen to have a look because that's his code