Name |
Last commit
|
Last update |
---|---|---|
.. | ||
barrier_client.v | ||
heap_lang.v | ||
joining_existentials.v | ||
list_reverse.v | ||
one_shot.v | ||
program_logic.v | ||
proofmode.v | ||
tree_sum.v |
This way type class inference is not invokved when used in tactics like iPvs while not having to write an @. (Idea suggested by Ralf.)
Name |
Last commit
|
Last update |
---|---|---|
.. | ||
barrier_client.v | Loading commit data... | |
heap_lang.v | Loading commit data... | |
joining_existentials.v | Loading commit data... | |
list_reverse.v | Loading commit data... | |
one_shot.v | Loading commit data... | |
program_logic.v | Loading commit data... | |
proofmode.v | Loading commit data... | |
tree_sum.v | Loading commit data... |