Commit 9b6f2c6e authored by Ralf Jung's avatar Ralf Jung
Browse files

tune some more priorities, to make sure we use Props_preo and Props_pcm

parent 1113f98e
...@@ -95,7 +95,7 @@ Section PUMMorphProps1. ...@@ -95,7 +95,7 @@ Section PUMMorphProps1.
unfold cchain; intros; apply σc; assumption. unfold cchain; intros; apply σc; assumption.
Qed. Qed.
Global Program Instance PMpreoT : preoType (T -m> U) := Global Program Instance PMpreoT : preoType (T -m> U) | 5:=
mkPOType (fun f g => forall x, (f x g x)%pd). mkPOType (fun f g => forall x, (f x g x)%pd).
Next Obligation. Next Obligation.
split. split.
...@@ -134,7 +134,7 @@ Section PUMMorphProps1. ...@@ -134,7 +134,7 @@ Section PUMMorphProps1.
Arguments PMEquiv _ _ /. Arguments PMEquiv _ _ /.
Global Instance mon_morph_preoT : pcmType (T -m> U). Global Instance mon_morph_preoT : pcmType (T -m> U) | 5.
Proof. Proof.
clear; split. clear; split.
- intros f1 f2 HEqf g1 g2 HEqg; split; intros HSub x; [symmetry in HEqf, HEqg |]; - intros f1 f2 HEqf g1 g2 HEqg; split; intros HSub x; [symmetry in HEqf, HEqg |];
......
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