-
Robbert Krebbers authored
This way type class inference is not invokved when used in tactics like iPvs while not having to write an @. (Idea suggested by Ralf.)
de9438cb
| 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 |