add 'Proof Using' hints to enable -quick compilation

theories/lang/adequacy.v

@@ -2,6 +2,7 @@ From iris.program_logic Require Export hoare adequacy.
 From iris.algebra Require Import auth.
 From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
+Set Default Proof Using "Type".
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_ownP :> ownPPreG lrust_lang Σ;

theories/lang/derived.v

 From lrust.lang Require Export lifting.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
+Set Default Proof Using "Type".
 Import uPred.
 
 (** Define some derived forms, and derived lemmas about them. *)

theories/lang/heap.v

@@ -4,6 +4,7 @@ From iris.algebra Require Import csum excl auth.
 From iris.base_logic Require Import big_op lib.invariants lib.fractional.
 From iris.proofmode Require Export tactics.
 From lrust.lang Require Export lifting.
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition heapN : namespace := nroot .@ "heap".

theories/lang/lang.v

 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
+Set Default Proof Using "Type".
 
 Open Scope Z_scope.
 

theories/lang/lifting.v

@@ -3,6 +3,7 @@ From iris.program_logic Require Import ectx_lifting.
 From lrust.lang Require Export lang.
 From lrust.lang Require Import tactics.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 Import uPred.
 Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
 

theories/lang/memcpy.v

 From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode.
+Set Default Proof Using "Type".
 
 Definition memcpy : val :=
   rec: "memcpy" ["dst";"len";"src"] :=

theories/lang/new_delete.v

 From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode memcpy.
+Set Default Proof Using "Type".
 
 Definition new : val :=
   λ: ["n"],

theories/lang/notation.v

 From lrust.lang Require Export derived.
+Set Default Proof Using "Type".
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.

theories/lang/proofmode.v

@@ -2,6 +2,7 @@ From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.base_logic Require Import namespaces.
 From lrust.lang Require Export wp_tactics heap.
+Set Default Proof Using "Type".
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.

theories/lang/races.v

@@ -2,6 +2,7 @@ From iris.prelude Require Import gmap.
 From iris.program_logic Require Export hoare.
 From iris.program_logic Require Import adequacy.
 From lrust.lang Require Import tactics.
+Set Default Proof Using "Type".
 
 Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
 

theories/lang/tactics.v

 From iris.prelude Require Import fin_maps.
 From lrust.lang Require Export lang.
+Set Default Proof Using "Type".
 
 (** We define an alternative representation of expressions in which the
 embedding of values and closed expressions is explicit. By reification of

theories/lang/wp_tactics.v

 From lrust.lang Require Export tactics derived.
+Set Default Proof Using "Type".
 Import uPred.
 
 (** wp-specific helper tactics *)

theories/lifetime/accessors.v

@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
+Set Default Proof Using "Type".
 
 Section accessors.
 Context `{invG Σ, lftG Σ}.

theories/lifetime/borrow.v

@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section borrow.
 Context `{invG Σ, lftG Σ}.

theories/lifetime/creation.v

@@ -4,6 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section creation.
 Context `{invG Σ, lftG Σ}.

theories/lifetime/definitions.v

@@ -3,6 +3,7 @@ From iris.prelude Require Export gmultiset strings.
 From iris.base_logic.lib Require Export invariants.
 From iris.base_logic.lib Require Import boxes.
 From iris.base_logic Require Import big_op.
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition lftN : namespace := nroot .@ "lft".

theories/lifetime/derived.v

 From lrust.lifetime Require Export primitive accessors faking.
 From lrust.lifetime Require Export raw_reborrow.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 (* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven
 in the model, depends on this file. *)
 

theories/lifetime/faking.v

@@ -3,6 +3,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Section faking.
 Context `{invG Σ, lftG Σ}.

theories/lifetime/frac_borrow.v

@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import lib.fractional.
 From iris.algebra Require Import frac.
 From lrust.lifetime Require Export shr_borrow .
+Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 

theories/lifetime/na_borrow.v

 From lrust.lifetime Require Export derived.
 From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 
 Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=