theories/heap_lang · edcdbc1dbc5e3338fd373f6d9804c8d6e9983110 · Simcha van Collem / Iris

Forked from Iris / Iris

5590 commits behind the upstream repository.

Try to start proofmode for all introduction tactics.

Robbert Krebbers authored 8 years ago

I also renamed `iProof` into `iStartProof`, as it is supposed to be
something internal, and not a substitute of Coq's `Proof` command (as
originally intended).

edcdbc1d

History

edcdbc1d 8 years ago

History

Name	Last commit	Last update
..
lib
adequacy.v
lang.v
lifting.v
notation.v
proofmode.v
tactics.v
wp_tactics.v