Skip to content
Snippets Groups Projects
Commit f72ef909 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

`Set Default Proof Using` is not needed due to `options`.

parent 4dcc0a1a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/algebra/dfrac.v
+ 0
− 2
View file @ f72ef909
...@@ -20,11 +20,9 @@ ...@@ -20,11 +20,9 @@
discarded. Conversely, knowing that a fraction has been discarded implies discarded. Conversely, knowing that a fraction has been discarded implies
that no one can own 1. And, since discarding is an irreversible operation, it 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 *) also implies that no one can own 1 in the future *)
From Coq.QArith Require Import Qcanon. From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra proofmode_classes updates. From iris.algebra Require Export cmra proofmode_classes updates.
From iris Require Import options. From iris Require Import options.
Set Default Proof Using "Type".
(** An element of dfrac denotes ownership of a fraction, knowledge that a (** 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 fraction has been discarded, or both. Note that all elements can be written
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment