Commit a3bcb51e authored by Ralf Jung's avatar Ralf Jung

tweak proofs

parent edbe48a7
Pipeline #14867 failed with stage
in 6 minutes and 11 seconds
......@@ -399,7 +399,7 @@ Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
if Qclt_le_dec x y then left _ else right _.
Solve Obligations with try done.
Next Obligation. done. Qed.
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
Instance: PartialOrder ().
......
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