From 18f29711a679b237cd945d4c667a2d66f42701ba Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Jan 2017 17:51:46 +0100
Subject: [PATCH] don't use Proof Using in a few files that get too many
unnecessary annotations from this
---
theories/algebra/cofe_solver.v | 3 ++-
theories/algebra/sts.v | 3 ++-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 84cb0b758..2527765eb 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -1,5 +1,6 @@
From iris.algebra Require Export ofe.
-Set Default Proof Using "Type*".
+(* FIXME: This file needs a 'Proof Using' hint, but the default we use
+ everywhere makes for lots of extra ssumptions. *)
Record solution (F : cFunctor) := Solution {
solution_car :> ofeT;
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index b52eca914..3f828a5d8 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,7 +1,8 @@
From iris.prelude Require Export set.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
-Set Default Proof Using "Type*".
+(* FIXME: This file needs a 'Proof Using' hint, but the default we use
+ everywhere makes for lots of extra ssumptions. *)
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
--
GitLab