Merge branch 'ralf/proofmode-import' into 'master'
use iris.proofmode.proofmode as the new root module for the proofmode See merge request iris/iris!724
Showing
- CHANGELOG.md 6 additions, 0 deletionsCHANGELOG.md
- _CoqProject 1 addition, 0 deletions_CoqProject
- iris/base_logic/bupd_alt.v 1 addition, 1 deletioniris/base_logic/bupd_alt.v
- iris/base_logic/lib/boxes.v 1 addition, 1 deletioniris/base_logic/lib/boxes.v
- iris/base_logic/lib/cancelable_invariants.v 1 addition, 1 deletioniris/base_logic/lib/cancelable_invariants.v
- iris/base_logic/lib/fancy_updates.v 1 addition, 1 deletioniris/base_logic/lib/fancy_updates.v
- iris/base_logic/lib/fancy_updates_from_vs.v 1 addition, 1 deletioniris/base_logic/lib/fancy_updates_from_vs.v
- iris/base_logic/lib/gen_heap.v 1 addition, 1 deletioniris/base_logic/lib/gen_heap.v
- iris/base_logic/lib/gen_inv_heap.v 1 addition, 1 deletioniris/base_logic/lib/gen_inv_heap.v
- iris/base_logic/lib/ghost_map.v 1 addition, 1 deletioniris/base_logic/lib/ghost_map.v
- iris/base_logic/lib/ghost_var.v 1 addition, 1 deletioniris/base_logic/lib/ghost_var.v
- iris/base_logic/lib/gset_bij.v 1 addition, 1 deletioniris/base_logic/lib/gset_bij.v
- iris/base_logic/lib/invariants.v 1 addition, 1 deletioniris/base_logic/lib/invariants.v
- iris/base_logic/lib/mono_nat.v 1 addition, 1 deletioniris/base_logic/lib/mono_nat.v
- iris/base_logic/lib/na_invariants.v 1 addition, 1 deletioniris/base_logic/lib/na_invariants.v
- iris/base_logic/lib/proph_map.v 1 addition, 1 deletioniris/base_logic/lib/proph_map.v
- iris/base_logic/lib/saved_prop.v 1 addition, 1 deletioniris/base_logic/lib/saved_prop.v
- iris/base_logic/lib/wsat.v 1 addition, 1 deletioniris/base_logic/lib/wsat.v
- iris/bi/lib/atomic.v 1 addition, 1 deletioniris/bi/lib/atomic.v
- iris/bi/lib/core.v 1 addition, 1 deletioniris/bi/lib/core.v
Loading
Please register or sign in to comment