From 5213177f215a95483c11142648e977f3c487f230 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Jan 2017 18:26:57 +0100
Subject: [PATCH] algebra.sts as the wrong file, the affected lemmas are in
 base_logic.lib.sts (already fixed by Robbert)

---
 theories/algebra/sts.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 3f828a5d8..b52eca914 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,8 +1,7 @@
 From iris.prelude Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
-(* FIXME: This file needs a 'Proof Using' hint, but the default we use
-   everywhere makes for lots of extra ssumptions. *)
+Set Default Proof Using "Type*".
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.
-- 
GitLab