We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent a7326f1 commit ff58d08Copy full SHA for ff58d08
src/phl/ecPhlPrRw.ml
@@ -89,7 +89,7 @@ let pr_sum env pr =
89
90
let pr_mu1_le_eq_mu1 m f args resv k fresh_id d =
91
let kfresh = f_local fresh_id k.f_ty in
92
- let f_ll = f_bdHoareF f_true f f_true FHeq f_r1
+ let f_ll = f_bdHoareF {m;inv=f_true} f {m;inv=f_true} FHeq {m;inv=f_r1}
93
and f_le_mu1 = f_forall [ (fresh_id, gtty k.f_ty) ]
94
(f_real_le (f_pr m f args (f_eq resv kfresh)) (f_mu_x d kfresh))
95
and concl =
0 commit comments