Commit 188c6e0c authored by Michael Sammler's avatar Michael Sammler
Browse files

add todos

parent ee88f0b6
......@@ -3,3 +3,6 @@
This repository contain a collection of interesting tricks and facts about Coq that were useful during the development of Iris.
- [simpl.v](theories/simpl.v): `simpl` and similar reduction insert casts even if they do not change the goal which can slow down Qed.
- TODO: How to use custom typeclass databases
- TODO: How to iterate over all solutions for typeclass search
- TODO: Causes for slow Qed times
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment