From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 contrib/correctness/pmisc.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/correctness/pmisc.ml')

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 29d8fdcf..076b11cd 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -8,7 +8,7 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliātre *)
 
-(* $Id: pmisc.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: pmisc.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Pp
 open Util
@@ -216,7 +216,7 @@ let rec type_v_knsubst s = function
 and type_c_knsubst s ((id,v),e,pl,q) =
   ((id, type_v_knsubst s v), e, 
    List.map (fun p -> { p with p_value = subst_mps s p.p_value }) pl,
-   option_app (fun q -> { q with a_value = subst_mps s q.a_value }) q)
+   option_map (fun q -> { q with a_value = subst_mps s q.a_value }) q)
 
 and binder_knsubst s (id,b) = 
   (id, match b with BindType v -> BindType (type_v_knsubst s v) | _ -> b)
-- 
cgit v1.2.3