program_logic · be7661979bc10938f0c9b0e716c080554b34901a · Ike Mulder / Iris

Forked from Iris / Iris

6131 commits behind the upstream repository.

Robbert Krebbers authored 8 years ago

This way we ensure that Coq gives an error message when one accidentially
writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of
lists.

be766197

History

be766197 8 years ago

History

Name	Last commit	Last update
..
adequacy.v
auth.v
boxes.v
cancelable_invariants.v
counter_examples.v
ectx_language.v
ectx_lifting.v
ectxi_language.v
ghost_ownership.v
hoare.v
invariants.v
iris.v
language.v
lifting.v
model.v
namespaces.v
ownership.v
pviewshifts.v
saved_prop.v
sts.v
thread_local.v
viewshifts.v
weakestpre.v