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

Typeclasses Opaque cannot yet be global

parent e73669ea
Branches
No related tags found
No related merge requests found
Pipeline #57027 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/lecture_notes/coq_intro_example_2.v
+ 1
− 1
View file @ ec3dadb8
...@@ -346,7 +346,7 @@ End monotone_counter. ...@@ -346,7 +346,7 @@ End monotone_counter.
(* Finally, we make the [isCounter] predicate opaque to typeclass search, which (* Finally, we make the [isCounter] predicate opaque to typeclass search, which
avoids expensive unfolding of abstract predicates in users of our specification. avoids expensive unfolding of abstract predicates in users of our specification.
*) *)
Global Typeclasses Opaque isCounter. Typeclasses Opaque isCounter.
(* In the preceding section we spent a lot of time defining our own resource (* In the preceding section we spent a lot of time defining our own resource
algebra and proving it satisfies all the needed properties. The same patterns algebra and proving it satisfies all the needed properties. The same patterns
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment