Skip to content
Snippets Groups Projects
Commit 52f09a60 authored by Janno's avatar Janno
Browse files

Make `unseal` TC opaque

parent 37eafc88
Branches
Tags
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment