From 0e3bc878ab81cd75c0d7b44a9309c198fe4402b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 6 Jan 2017 13:57:10 +0100
Subject: [PATCH] add 'Proof Using' hints to enable -quick compilation

---
 theories/lang/adequacy.v         | 1 +
 theories/lang/derived.v          | 1 +
 theories/lang/heap.v             | 1 +
 theories/lang/lang.v             | 1 +
 theories/lang/lifting.v          | 1 +
 theories/lang/memcpy.v           | 1 +
 theories/lang/new_delete.v       | 1 +
 theories/lang/notation.v         | 1 +
 theories/lang/proofmode.v        | 1 +
 theories/lang/races.v            | 1 +
 theories/lang/tactics.v          | 1 +
 theories/lang/wp_tactics.v       | 1 +
 theories/lifetime/accessors.v    | 1 +
 theories/lifetime/borrow.v       | 1 +
 theories/lifetime/creation.v     | 1 +
 theories/lifetime/definitions.v  | 1 +
 theories/lifetime/derived.v      | 1 +
 theories/lifetime/faking.v       | 1 +
 theories/lifetime/frac_borrow.v  | 1 +
 theories/lifetime/na_borrow.v    | 1 +
 theories/lifetime/primitive.v    | 1 +
 theories/lifetime/raw_reborrow.v | 1 +
 theories/lifetime/reborrow.v     | 1 +
 theories/lifetime/shr_borrow.v   | 1 +
 theories/typing/bool.v           | 1 +
 theories/typing/borrow.v         | 1 +
 theories/typing/cont.v           | 1 +
 theories/typing/cont_context.v   | 1 +
 theories/typing/fixpoint.v       | 1 +
 theories/typing/function.v       | 1 +
 theories/typing/int.v            | 1 +
 theories/typing/lft_contexts.v   | 1 +
 theories/typing/own.v            | 1 +
 theories/typing/product.v        | 1 +
 theories/typing/product_split.v  | 1 +
 theories/typing/programs.v       | 1 +
 theories/typing/shr_bor.v        | 1 +
 theories/typing/sum.v            | 1 +
 theories/typing/tests/get_x.v    | 1 +
 theories/typing/type.v           | 1 +
 theories/typing/type_context.v   | 1 +
 theories/typing/type_sum.v       | 1 +
 theories/typing/uninit.v         | 1 +
 theories/typing/uniq_bor.v       | 1 +
 44 files changed, 44 insertions(+)

diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 58e72cf0..e402dc73 100644
--- a/theories/lang/adequacy.v
+++ b/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 Σ;
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 00d92652..a649ab18 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -1,6 +1,7 @@
 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. *)
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 679e3a9b..a976118a 100644
--- a/theories/lang/heap.v
+++ b/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".
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index af91c92d..e770632f 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -1,6 +1,7 @@
 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.
 
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index cfd392c0..ede4cd0f 100644
--- a/theories/lang/lifting.v
+++ b/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.
 
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index e65919f1..f11083b0 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -1,6 +1,7 @@
 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"] :=
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index fa541f0f..5b5be827 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -1,6 +1,7 @@
 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"],
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index a47399b5..1caf26f4 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -1,4 +1,5 @@
 From lrust.lang Require Export derived.
+Set Default Proof Using "Type".
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index fb4d20e8..44a89ce8 100644
--- a/theories/lang/proofmode.v
+++ b/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.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index dc94392d..c0b8b497 100644
--- a/theories/lang/races.v
+++ b/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.
 
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index a622fdda..5767645f 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,5 +1,6 @@
 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
diff --git a/theories/lang/wp_tactics.v b/theories/lang/wp_tactics.v
index 12d8f8ca..f4d6c053 100644
--- a/theories/lang/wp_tactics.v
+++ b/theories/lang/wp_tactics.v
@@ -1,4 +1,5 @@
 From lrust.lang Require Export tactics derived.
+Set Default Proof Using "Type".
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index 14210f73..2f3b4b03 100644
--- a/theories/lifetime/accessors.v
+++ b/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 Σ}.
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index b2bf7ce8..7ce44ada 100644
--- a/theories/lifetime/borrow.v
+++ b/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 Σ}.
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 5c4cb539..e731f97a 100644
--- a/theories/lifetime/creation.v
+++ b/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 Σ}.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index d98f4dd1..ce443fd3 100644
--- a/theories/lifetime/definitions.v
+++ b/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".
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 73b28d10..ecf3524f 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -1,6 +1,7 @@
 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. *)
 
diff --git a/theories/lifetime/faking.v b/theories/lifetime/faking.v
index 7ee7bd10..1def1f51 100644
--- a/theories/lifetime/faking.v
+++ b/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 Σ}.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 841ac12e..77084d69 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/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.
 
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 16ae3d69..41a69f9e 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -1,6 +1,7 @@
 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 Σ) :=
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 235510a1..7ed8780a 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.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 fractional.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
 Import uPred.
 
 Section primitive.
diff --git a/theories/lifetime/raw_reborrow.v b/theories/lifetime/raw_reborrow.v
index cde623f0..7dbf4a55 100644
--- a/theories/lifetime/raw_reborrow.v
+++ b/theories/lifetime/raw_reborrow.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 rebor.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/reborrow.v b/theories/lifetime/reborrow.v
index b8990644..567d6b42 100644
--- a/theories/lifetime/reborrow.v
+++ b/theories/lifetime/reborrow.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 reborrow.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 0df3676d..10a14731 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Import gmap auth frac.
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Export derived.
+Set Default Proof Using "Type".
 
 (** Shared bors  *)
 Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 9f828788..60330dce 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -2,6 +2,7 @@ From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
 
 Section bool.
   Context `{typeG Σ}.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 13baa93e..e105e2cd 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -4,6 +4,7 @@ From lrust.lifetime Require Import reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
+Set Default Proof Using "Type".
 
 (** The rules for borrowing and derferencing borrowed non-Copy pointers are in
   a separate file so make sure that own.v and uniq_bor.v can be compiled
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 10926c2f..85319486 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
 
 Section typing.
   Context `{typeG Σ}.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b3fb8b95..e239890b 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -3,6 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
 From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts type_context.
+Set Default Proof Using "Type".
 
 Section cont_context_def.
   Context `{typeG Σ}.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 2cb0e1b4..c8ca59f8 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,5 +1,6 @@
 From lrust.lifetime Require Import definitions.
 From lrust.typing Require Export lft_contexts type bool.
+Set Default Proof Using "Type".
 
 Section fixpoint.
   Context `{typeG Σ}.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 95981845..709fe8b8 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import vector.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs cont.
+Set Default Proof Using "Type".
 
 Section fn.
   Context `{typeG Σ} {A : Type} {n : nat}.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 5b4cc7e3..27d58cf4 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import bool programs.
+Set Default Proof Using "Type".
 
 Section int.
   Context `{typeG Σ}.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 76e72e94..1fa4444e 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import fractional.
 From lrust.lifetime Require Import derived borrow frac_borrow.
+Set Default Proof Using "Type".
 
 Inductive elctx_elt : Type :=
 | ELCtx_Alive (κ : lft)
diff --git a/theories/typing/own.v b/theories/typing/own.v
index a2a94267..c095a2a7 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -6,6 +6,7 @@ From lrust.lang Require Export new_delete.
 From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import uninit type_context programs.
+Set Default Proof Using "Type".
 
 Section own.
   Context `{typeG Σ}.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 705ae108..bed77182 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
+Set Default Proof Using "Type".
 
 Section product.
   Context `{typeG Σ}.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 261a2d36..b02d8d1d 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -4,6 +4,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
+Set Default Proof Using "Type".
 
 Section product_split.
   Context `{typeG Σ}.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index e5ae5ee4..4ff553ea 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -3,6 +3,7 @@ From lrust.lang Require Export notation.
 From lrust.lang Require Import proofmode memcpy.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
+Set Default Proof Using "Type".
 
 Section typing.
   Context `{typeG Σ}.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 789aaa3e..23350e74 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import frac_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context programs.
+Set Default Proof Using "Type".
 
 Section shr_bor.
   Context `{typeG Σ}.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 6cb8c72a..330da63d 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -3,6 +3,7 @@ From iris.algebra Require Import list.
 From iris.base_logic Require Import fractional.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
+Set Default Proof Using "Type".
 
 Section sum.
   Context `{typeG Σ}.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index b7e263d2..d770fb2a 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -2,6 +2,7 @@ From lrust.lifetime Require Import definitions.
 From lrust.lang Require Import new_delete.
 From lrust.typing Require Import programs product product_split own uniq_bor
                     shr_bor int function lft_contexts uninit cont.
+Set Default Proof Using "Type".
 
 Section get_x.
   Context `{typeG Σ}.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 88bb1ddd..8585d230 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -3,6 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.typing Require Import lft_contexts.
+Set Default Proof Using "Type".
 
 Class typeG Σ := TypeG {
   type_heapG :> heapG Σ;
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 9344e92e..741e0558 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -3,6 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
 From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts.
+Set Default Proof Using "Type".
 
 Definition path := expr.
 Bind Scope expr_scope with path.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index e523544d..eece54ef 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -3,6 +3,7 @@ From lrust.lang Require Import heap memcpy.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
 From lrust.typing Require Import lft_contexts type_context programs product.
+Set Default Proof Using "Type".
 
 Section case.
   Context `{typeG Σ}.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 6c25430d..0dbfa1ea 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import product.
+Set Default Proof Using "Type".
 
 Section uninit.
   Context `{typeG Σ}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 5920a3c2..8c776efa 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -4,6 +4,7 @@ From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context shr_bor programs.
+Set Default Proof Using "Type".
 
 Section uniq_bor.
   Context `{typeG Σ}.
-- 
GitLab