From 8078f356a19951b5ca0c19d4aa79f75fee702744 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 19 Jun 2020 09:01:40 +0200
Subject: [PATCH] update dependencies; import numbers where needed and update
 Makefile

---
 Makefile                                          | 2 +-
 opam                                              | 2 +-
 theories/lang/heap.v                              | 2 +-
 theories/lang/lib/arc.v                           | 2 +-
 theories/lifetime/model/creation.v                | 2 +-
 theories/lifetime/model/definitions.v             | 2 +-
 theories/lifetime/model/faking.v                  | 2 +-
 theories/lifetime/model/reborrow.v                | 2 +-
 theories/typing/lib/rc/rc.v                       | 2 +-
 theories/typing/lib/rc/weak.v                     | 2 +-
 theories/typing/lib/refcell/ref_code.v            | 2 +-
 theories/typing/lib/refcell/refcell.v             | 2 +-
 theories/typing/lib/refcell/refmut_code.v         | 2 +-
 theories/typing/lib/rwlock/rwlock.v               | 2 +-
 theories/typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
 theories/typing/product.v                         | 2 +-
 theories/typing/product_split.v                   | 1 +
 theories/typing/type.v                            | 1 +
 18 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/Makefile b/Makefile
index 8d615e4b..331cb03f 100644
--- a/Makefile
+++ b/Makefile
@@ -8,7 +8,7 @@ all: Makefile.coq
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
-	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
 	rm -f Makefile.coq .lia.cache
 .PHONY: clean
 
diff --git a/opam b/opam
index 62928aa1..f75b6de6 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-05-26.1.d80e7abf") | (= "dev") }
+  "coq-iris" { (= "dev.2020-06-18.3.5f98a0bf") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 3ad8e893..8f24ca2d 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -1,6 +1,6 @@
 From Coq Require Import Min.
 From stdpp Require Import coPset.
-From iris.algebra Require Import big_op gmap frac agree.
+From iris.algebra Require Import big_op gmap frac agree numbers.
 From iris.algebra Require Import csum excl auth cmra_big_op.
 From iris.bi Require Import fractional.
 From iris.base_logic Require Export lib.own.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 5ed568ef..203abf73 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Import weakestpre.
 From iris.proofmode Require Import tactics.
 From iris.bi Require Import fractional.
-From iris.algebra Require Import excl csum frac auth.
+From iris.algebra Require Import excl csum frac auth numbers.
 From lrust.lang Require Import lang proofmode notation new_delete.
 Set Default Proof Using "Type".
 
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 622f63e9..383ed012 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Import faking.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 44a336f5..0bf99ce9 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
 From lrust.lifetime Require Export lifetime_sig.
 Set Default Proof Using "Type".
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 7236c894..668036e2 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -1,5 +1,5 @@
 From lrust.lifetime Require Export primitive.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index a6ad7bb0..0802fcea 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,5 +1,5 @@
 From lrust.lifetime Require Import borrow accessors.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index d2428f7b..ddf5a893 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree excl.
+From iris.algebra Require Import auth csum frac agree excl numbers.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index ded42fd5..e79b7885 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 87fae82d..7dc10476 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index ac94210f..c8acaf22 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index f40cfa8a..d793d41e 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 027bc151..7ed012d3 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree excl.
+From iris.algebra Require Import auth csum frac agree excl numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 2eb1f1c2..ebf0a8e7 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 7076ceaa..42bed577 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import list.
+From iris.algebra Require Import list numbers.
 From lrust.typing Require Import lft_contexts.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index ac417767..4463e0d1 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,4 +1,5 @@
 From Coq Require Import Qcanon.
+From iris.algebra Require Import numbers.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index c969d758..9da92246 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import numbers.
 From iris.base_logic.lib Require Export na_invariants.
 From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Export frac_borrow.
-- 
GitLab