Skip to content
Snippets Groups Projects
Commit 36874919 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'janno/tc-opaque-unseal' into 'master' 

Make `unseal` TC opaque

See merge request !487
parents b9418660 b36b4c3a
No related branches found
No related tags found
1 merge request!487Make `unseal` TC opaque
Pipeline #88982 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 0 deletions
stdpp/base.v
+ 1
− 0
View file @ 36874919
...@@ -56,6 +56,7 @@ Add Search Blacklist "_unseal". ...@@ -56,6 +56,7 @@ Add Search Blacklist "_unseal".
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }. Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
Global Arguments unseal {_ _} _ : assert. Global Arguments unseal {_ _} _ : assert.
Global Arguments seal_eq {_ _} _ : assert. Global Arguments seal_eq {_ _} _ : assert.
Global Typeclasses Opaque unseal.
(** * Solving type class instances *) (** * Solving type class instances *)
(** The tactic [tc_solve] is used to solve type class goals by invoking type (** The tactic [tc_solve] is used to solve type class goals by invoking type
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment