Commit ee3e02f0 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers

don't use Proof Using in a few files that get too many unnecessary annotations from this

parent 2028fae1
...@@ -4,7 +4,8 @@ ...@@ -4,7 +4,8 @@
importantly, it implements some tactics to automatically solve goals involving importantly, it implements some tactics to automatically solve goals involving
collections. *) collections. *)
From stdpp Require Export orders list. 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, Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
x, x X x Y. x, x X x Y.
......
...@@ -6,7 +6,8 @@ induction principles for finite maps and implements the tactic ...@@ -6,7 +6,8 @@ induction principles for finite maps and implements the tactic
[simplify_map_eq] to simplify goals involving finite maps. *) [simplify_map_eq] to simplify goals involving finite maps. *)
From Coq Require Import Permutation. From Coq Require Import Permutation.
From stdpp Require Export relations orders vector. 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 *) (** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of (** We require Leibniz equality to be extensional on finite maps. This of
......
Markdown is supported
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