Compare revisions

0f4ebd6d · 0f4ebd6d · 0f4ebd6d · 0f4ebd6d · 0f4ebd6d · 0f4ebd6d
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -3,3 +3,4 @@ From lrust.typing Require Export
  lft_contexts type_context cont_context programs cont type
  int bool own uniq_bor shr_bor uninit product sum fixpoint function
  product_split borrow type_sum.
+From iris.prelude Require Import options.
No results found