Skip to content
Snippets Groups Projects

Make `unseal` TC opaque

Merged Janno requested to merge janno/tc-opaque-unseal into master
All threads resolved!
1 file
+ 1
1
Compare changes
  • Side-by-side
  • Inline
+ 1
0
@@ -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
Loading