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

Fix build by being a little bit less restrictive in Hint Modes.

parent b4b06bc7
...@@ -38,7 +38,8 @@ Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := { ...@@ -38,7 +38,8 @@ Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
embed_later P : ⎡▷ P P; embed_later P : ⎡▷ P P;
embed_interal_inj (PROP' : sbi) (P Q : PROP1) : P Q (P Q : PROP'); embed_interal_inj (PROP' : sbi) (P Q : PROP1) : P Q (P Q : PROP');
}. }.
Hint Mode SbiEmbed + + ! : typeclass_instances. Hint Mode SbiEmbed ! - - : typeclass_instances.
Hint Mode SbiEmbed - ! - : typeclass_instances.
Section embed_laws. Section embed_laws.
Context `{BiEmbed PROP1 PROP2}. Context `{BiEmbed PROP1 PROP2}.
......
...@@ -48,7 +48,7 @@ Class BiPlainlyExist `{!BiPlainly PROP} := ...@@ -48,7 +48,7 @@ Class BiPlainlyExist `{!BiPlainly PROP} :=
Arguments BiPlainlyExist : clear implicits. Arguments BiPlainlyExist : clear implicits.
Arguments BiPlainlyExist _ {_}. Arguments BiPlainlyExist _ {_}.
Arguments plainly_exist_1 _ {_ _} _. Arguments plainly_exist_1 _ {_ _} _.
Hint Mode BiPlainlyExist + ! : typeclass_instances. Hint Mode BiPlainlyExist ! - : typeclass_instances.
Section plainly_laws. Section plainly_laws.
Context `{BiPlainly PROP}. Context `{BiPlainly PROP}.
......
...@@ -87,11 +87,11 @@ Arguments bi_fupd_fupd : simpl never. ...@@ -87,11 +87,11 @@ Arguments bi_fupd_fupd : simpl never.
Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} := Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} :=
bupd_fupd E (P : PROP) : (|==> P) ={E}= P. bupd_fupd E (P : PROP) : (|==> P) ={E}= P.
Hint Mode BiBUpdFUpd + ! ! : typeclass_instances. Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} := Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
bupd_plainly (P : PROP) : (|==> P) - P. bupd_plainly (P : PROP) : (|==> P) - P.
Hint Mode BiBUpdPlainly + ! ! : typeclass_instances. Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := { Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} : fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
...@@ -100,7 +100,7 @@ Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := { ...@@ -100,7 +100,7 @@ Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
later_fupd_plain E (P : PROP) `{!Plain P} : later_fupd_plain E (P : PROP) `{!Plain P} :
( |={E}=> P) ={E}= P; ( |={E}=> P) ={E}= P;
}. }.
Hint Mode BiBUpdFUpd + ! ! : typeclass_instances. Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Section bupd_laws. Section bupd_laws.
Context `{BiBUpd PROP}. Context `{BiBUpd PROP}.
......
Supports Markdown
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