Commit fa25e2cc authored by Ralf Jung's avatar Ralf Jung

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

parent 65b9ce9f
......@@ -198,4 +198,6 @@ Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
Proof. iIntros (HP) "H". iApply (recv_weaken with "[] H"). iApply HP. Qed.
End proof.
SearchAbout _.
Typeclasses Opaque barrier_ctx send recv.
......@@ -4,7 +4,8 @@
importantly, it implements some tactics to automatically solve goals involving
collections. *)
From iris.prelude 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.
......
......@@ -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 iris.prelude 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
......
(** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language weakestpre lifting.
From iris.proofmode Require Import tactics.
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. *)
Section wp.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
......
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