diff options
Diffstat (limited to 'contrib/correctness/pwp.ml')
| -rw-r--r-- | contrib/correctness/pwp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml index 1e485180..f422c5cd 100644 --- a/contrib/correctness/pwp.ml +++ b/contrib/correctness/pwp.ml @@ -8,7 +8,7 @@ (* Certification of Imperative Programs / Jean-Christophe Filliātre *) -(* $Id: pwp.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: pwp.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Util open Names @@ -64,7 +64,7 @@ let update_post env top ef c = let force_post up env top q e = let (res,ef,p,_) = e.info.kappa in let q' = - if up then option_app (named_app (update_post env top ef)) q else q + if up then option_map (named_app (update_post env top ef)) q else q in let i = { env = e.info.env; kappa = (res,ef,p,q') } in { desc = e.desc; pre = e.pre; post = q'; loc = e.loc; info = i } @@ -260,7 +260,7 @@ and propagate ren p = | Apply (f,l) -> let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in if ok then - let q = option_app (named_app (real_subst_in_constr so)) qapp in + let q = option_map (named_app (real_subst_in_constr so)) qapp in post_if_none env q p else p @@ -285,7 +285,7 @@ and propagate ren p = None -> Some (anonymous s) | Some i -> Some { a_value = conj i.a_value s; a_name = i.a_name } in - let q = option_app (named_app abstract_unit) q in + let q = option_map (named_app abstract_unit) q in post_if_none env q p | SApp ([Variable id], [e1;e2]) |