From ee3e02f09ec73577ffe4fa02df31805d2983b9af Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 4 Jan 2017 17:47:46 +0100
Subject: [PATCH] don't use Proof Using in a few files that get too many
unnecessary annotations from this
---
theories/collections.v | 3 ++-
theories/fin_maps.v | 3 ++-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/theories/collections.v b/theories/collections.v
index 1a34474..e4856b5 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -4,7 +4,8 @@
importantly, it implements some tactics to automatically solve goals involving
collections. *)
From stdpp Require Export orders list.
-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. *)
Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
∀ x, x ∈ X ↔ x ∈ Y.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index cc85921..89b5ebe 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -6,7 +6,8 @@ induction principles for finite maps and implements the tactic
[simplify_map_eq] to simplify goals involving finite maps. *)
From Coq Require Import Permutation.
From stdpp Require Export relations orders vector.
-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. *)
(** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of
--
GitLab