Commit 8ff30e0f authored by Ralf Jung's avatar Ralf Jung

move Arguments out of section

parent 2131d528
Pipeline #4656 passed with stages
in 5 minutes and 13 seconds
......@@ -21,9 +21,9 @@ Add Search Blacklist "_obligation_".
Section seal.
Local Set Primitive Projections.
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert.
End seal.
Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert.
(** Typeclass opaque definitions *)
(* The constant [tc_opaque] is used to make definitions opaque for just type
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment