Commit ad06e03a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix type of monPred_bi_embedding and monPred_sbi_embedding.

parent 86bb4fb3
......@@ -469,7 +469,7 @@ Proof.
Qed.
Global Instance monPred_bi_embedding :
Inhabited I @BiEmbedding PROP (monPredI I PROP) bi_embed.
Inhabited I BiEmbedding PROP (monPredI I PROP).
Proof.
split; try apply _; unseal; try done.
- move =>?? /= [/(_ inhabitant) ?] //.
......@@ -502,6 +502,6 @@ Proof.
Qed.
Global Instance monPred_sbi_embedding :
Inhabited I @SbiEmbedding PROP (monPredSI I PROP) bi_embed.
Inhabited I SbiEmbedding PROP (monPredSI I PROP).
Proof. split; try apply _. by unseal. Qed.
End sbi_facts.
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