diff --git a/stdpp/base.v b/stdpp/base.v index 4aaf037604acf23d13fe0806fd5d61df7e9e5859..29f1d074ff4fb6ac1e99bfad531207988eee56fd 100644 --- a/stdpp/base.v +++ b/stdpp/base.v @@ -56,6 +56,7 @@ Add Search Blacklist "_unseal". Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }. Global Arguments unseal {_ _} _ : assert. Global Arguments seal_eq {_ _} _ : assert. +Global Typeclasses Opaque unseal. (** * Solving type class instances *) (** The tactic [tc_solve] is used to solve type class goals by invoking type