diff options
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) |