diff options
author | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
commit | 35335c0605a84770f93965ea6b315cd369e9b731 (patch) | |
tree | 87b219b3275f8e21e88ed2970da3c056bc8f19e6 /contrib/correctness/pwp.ml | |
parent | fe730babfe0c01baa6c6da62460938f8839aa7c6 (diff) | |
parent | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (diff) |
Merge commit 'upstream/8.0pl3+8.1beta' into 8.1
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]) |