update dependencies; import numbers where needed and update Makefile

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
 

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}%"]

theories/lang/heap.v

 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.

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".
 

theories/lifetime/model/creation.v

 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".

theories/lifetime/model/definitions.v

-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".

theories/lifetime/model/faking.v

 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".

theories/lifetime/model/reborrow.v

 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".

theories/typing/lib/rc/rc.v

 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.

theories/typing/lib/rc/weak.v

 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.

theories/typing/lib/refcell/ref_code.v

 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.

theories/typing/lib/refcell/refcell.v

 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.

theories/typing/lib/refcell/refmut_code.v

 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.

theories/typing/lib/rwlock/rwlock.v

 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.

theories/typing/lib/rwlock/rwlockreadguard_code.v

 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.

theories/typing/product.v

 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".

theories/typing/product_split.v

 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.

theories/typing/type.v

+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.