From 61d11c649b4cd68e92861e2fea86f6c6a6b5bb6a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 27 Apr 2006 19:37:33 +0000
Subject: Standardisation nom option_app en option_map

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml     | 2 +-
 library/declaremods.ml | 2 +-
 library/lib.ml         | 2 +-
 library/libobject.ml   | 4 ++--
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 3835180b16..343bc0c508 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -204,7 +204,7 @@ let hcons_constant_declaration = function
       let (hcons1_constr,_) = hcons_constr (hcons_names()) in
       DefinitionEntry
        { const_entry_body = hcons1_constr ce.const_entry_body;
-	 const_entry_type = option_app hcons1_constr ce.const_entry_type;
+	 const_entry_type = option_map hcons1_constr ce.const_entry_type;
          const_entry_opaque = ce.const_entry_opaque; 
          const_entry_boxed = ce.const_entry_boxed }
   | cd -> cd
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 39b9fc643e..658ca4afb4 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -585,7 +585,7 @@ let register_library dir cenv objs digest =
 	  let msid,substitute,keep = objs in
 	  let substobjs = empty_subst, [], msid, substitute in
 	  let substituted = subst_substobjs dir mp substobjs in
-	  let objects = option_app (fun seg -> seg@keep) substituted in
+	  let objects = option_map (fun seg -> seg@keep) substituted in
 	  let modobjs = substobjs, objects in
 	    Hashtbl.add library_cache dir modobjs;
 	    modobjs
diff --git a/library/lib.ml b/library/lib.ml
index d1bb6599ad..bc01c4776d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -460,7 +460,7 @@ let open_section id =
 
 let discharge_item = function
   | ((sp,_ as oname),Leaf lobj) ->
-      option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+      option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
   | _ ->
       None
 
diff --git a/library/libobject.ml b/library/libobject.ml
index d84e0bc26f..b91cbe699b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -109,12 +109,12 @@ let declare_object odecl =
       anomaly "somehow we got the wrong dynamic object in the classifyfun"
   and discharge (oname,lobj) = 
     if Dyn.tag lobj = na then 
-      option_app infun (odecl.discharge_function (oname,outfun lobj))
+      option_map infun (odecl.discharge_function (oname,outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
-      option_app infun (odecl.export_function (outfun lobj))
+      option_map infun (odecl.export_function (outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the exportfun"
 
-- 
cgit v1.2.3