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 | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /contrib/correctness/pmonad.ml | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'contrib/correctness/pmonad.ml')
-rw-r--r-- | contrib/correctness/pmonad.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml index 31effc1b..8f1b5946 100644 --- a/contrib/correctness/pmonad.ml +++ b/contrib/correctness/pmonad.ml @@ -8,7 +8,7 @@ (* Certification of Imperative Programs / Jean-Christophe Filliātre *) -(* $Id: pmonad.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: pmonad.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Util open Names @@ -76,9 +76,9 @@ let rec abstract_post ren env (e,q) = let after_id id = id_of_string ((string_of_id id) ^ "'") in let (_,go) = Peffect.get_repr e in let al = List.map (fun id -> (id,after_id id)) go in - let q = option_app (named_app (subst_in_constr al)) q in + let q = option_map (named_app (subst_in_constr al)) q in let tgo = List.map (fun (id,aid) -> (aid, trad_type_in_env ren env id)) al in - option_app (named_app (abstract tgo)) q + option_map (named_app (abstract tgo)) q (* Translation of effects types in cic types. * @@ -365,7 +365,7 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c = @(eq_phi ren'' env s svi tf) @(List.map (fun c -> CC_hole c) holes)) in - let qapp' = option_app (named_app (subst_in_constr svi)) qapp in + let qapp' = option_map (named_app (subst_in_constr svi)) qapp in let t = make_let_in ren'' env fe [] (current_vars ren''' outf,qapp') (res,tyres) (t,ty) |