Skip to content
Snippets Groups Projects

Tree Borrows update

Merged Neven Villani requested to merge ci/tree-borrows into master
Compare and
63 files
+ 2180
8837
Compare changes
  • Side-by-side
  • Inline
Files
63
(** This file has been adapted from the Stacked Borrows development, available at
https://gitlab.mpi-sws.org/FP/stacked-borrows
*)
From simuliris.simulation Require Import lifting.
From simuliris.tree_borrows Require Import primitive_laws proofmode examples.lib adequacy.
From iris.prelude Require Import options.
@@ -127,8 +123,10 @@ Section closed.
Qed.
End closed.
(*
Check prot_mutable_reorder_read_down_ctx.
Print Assumptions prot_mutable_reorder_read_down_ctx.
*)
(*
prot_mutable_reorder_read_down_ctx
: ctx_ref prot_mutable_reorder_read_down_opt prot_mutable_reorder_read_down_unopt
Loading