From f72ef909975c143815e7f8a11646228543663c81 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 3 Oct 2020 20:01:11 +0200
Subject: [PATCH] `Set Default Proof Using` is not needed due to `options`.

---
 theories/algebra/dfrac.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index 0a17ebb72..23f7242a0 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -20,11 +20,9 @@
     discarded. Conversely, knowing that a fraction has been discarded implies
     that no one can own 1. And, since discarding is an irreversible operation, it
     also implies that no one can own 1 in the future *)
-
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra proofmode_classes updates.
 From iris Require Import options.
-Set Default Proof Using "Type".
 
 (** An element of dfrac denotes ownership of a fraction, knowledge that a
     fraction has been discarded, or both. Note that all elements can be written
-- 
GitLab