Commit b4b06bc7 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix build.

parent 15425e74
......@@ -38,7 +38,7 @@ Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
embed_later P : ⎡▷ P P;
embed_interal_inj (PROP' : sbi) (P Q : PROP1) : P Q (P Q : PROP');
}.
Hint Mode BiEmbed + + ! ! : typeclass_instances.
Hint Mode SbiEmbed + + ! : typeclass_instances.
Section embed_laws.
Context `{BiEmbed PROP1 PROP2}.
......
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