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

6 files changed, 29 insertions, 29 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5efa68e2d..4fbeff526 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -680,7 +680,7 @@ let rec extern inctx scopes vars r =
       let vars' = 
 	List.fold_right (name_fold Idset.add)
 	  (cases_predicate_names tml) vars in
-      let rtntypopt' = option_app (extern_typ scopes vars') rtntypopt in
+      let rtntypopt' = option_map (extern_typ scopes vars') rtntypopt in
       let tml = List.map (fun (tm,(na,x)) ->
         let na' = match na,tm with
             Anonymous, RVar (_,id) when 
@@ -690,7 +690,7 @@ let rec extern inctx scopes vars r =
           | Name id, RVar (_,id') when id=id' -> None
           | Name _, _ -> Some na in
 	(sub_extern false scopes vars tm,
-	(na',option_app (fun (loc,ind,nal) ->
+	(na',option_map (fun (loc,ind,nal) ->
 	  let args = List.map (function
 	    | Anonymous -> RHole (dummy_loc,Evd.InternalHole) 
 	    | Name id -> RVar (dummy_loc,id)) nal in
@@ -701,15 +701,15 @@ let rec extern inctx scopes vars r =
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,nal,
-        (option_app (fun _ -> na) typopt,
-         option_app (extern_typ scopes (add_vname vars na)) typopt),
+        (option_map (fun _ -> na) typopt,
+         option_map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
-        (option_app (fun _ -> na) typopt,
-         option_app (extern_typ scopes (add_vname vars na)) typopt),
+        (option_map (fun _ -> na) typopt,
+         option_map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars b1, sub_extern false scopes vars b2)
 
   | RRec (loc,fk,idv,blv,tyv,bv) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index aa2c91b20..376360046 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -879,21 +879,21 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	    let (tm,ind),nal = intern_case_item env citm in
 	    (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
 	  tms ([],env) in
-        let rtnpo = option_app (intern_type env') rtnpo in
+        let rtnpo = option_map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	RCases (loc, rtnpo, tms, List.flatten eqns')
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
         let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = option_app (intern_type env'') po in
+        let p' = option_map (intern_type env'') po in
         RLetTuple (loc, nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) env nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
         let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = option_app (intern_type env'') po in
+        let p' = option_map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
 	RHole (loc, Evd.QuestionMark)
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 385171fe3..2c38b4c79 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -220,7 +220,7 @@ let app_list1 f = function
 let app_opt f = function
   | (OptArgType t as u, l) ->
       let o = Obj.magic l in
-      (u, Obj.repr (option_app (fun x -> out_gen t (f (in_gen t x))) o))
+      (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o))
   | _ -> failwith "Genarg: not an opt"
 
 let app_pair f1 f2 = function
diff --git a/interp/notation.ml b/interp/notation.ml
index d068cf64c..74263b768 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -234,12 +234,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x))
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
-    (patl, (fun r -> option_app mkNumeral (uninterp r)), inpat)
+    (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
-    (patl, (fun r -> option_app mkString (uninterp r)), inpat)
+    (patl, (fun r -> option_map mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.absolute_reference sp in ()
@@ -389,7 +389,7 @@ let uninterp_prim_token_cases_pattern c =
 
 let availability_of_prim_token printer_scope scopes =
   let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
-  option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
+  option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
 (* Miscellaneous *)
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 834587f8d..85f188599 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -59,17 +59,17 @@ let rec unloc = function
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
   | RCases (_,rtntypopt,tml,pl) ->
       RCases (dummy_loc,
-        (option_app unloc rtntypopt),
+        (option_map unloc rtntypopt),
 	List.map (fun (tm,x) -> (unloc tm,x)) tml,
         List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
   | RLetTuple (_,nal,(na,po),b,c) ->
-      RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
+      RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c)
   | RIf (_,c,(na,po),b1,b2) ->
-      RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
+      RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2)
   | RRec (_,fk,idl,bl,tyl,bv) ->
       RRec (dummy_loc,fk,idl,
             Array.map (List.map 
-              (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty)))
+              (fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty)))
               bl,
             Array.map unloc tyl,
             Array.map unloc bv)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d82c04e07..cc84d0c10 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -86,14 +86,14 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let eqnl' = List.map (fun (idl,pat,rhs) ->
         let (idl,e) = List.fold_right fold idl ([],e) in
 	(loc,idl,pat,f e rhs)) eqnl in
-      RCases (loc,option_app (f e') rtntypopt,tml',eqnl')
+      RCases (loc,option_map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
       let e,nal = list_fold_map (name_app g) e nal in 
       let e,na = name_app g e na in
-      RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c)
+      RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c)
   | AIf (c,(na,po),b1,b2) ->
       let e,na = name_app g e na in
-      RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2)
+      RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
   | ACast (c,k,t) -> RCast (loc,f e c,k,f e t)
   | ASort x -> RSort (loc,x)
   | AHole x  -> RHole (loc,x)
@@ -182,20 +182,20 @@ let aconstr_and_vars_of_rawconstr a =
       let f (_,idl,pat,rhs) =
         found := idl@(!found);
         (idl,pat,aux rhs) in
-      ACases (option_app aux rtntypopt,
+      ACases (option_map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  option_iter
 	    (fun (_,_,nl) -> List.iter (add_name found) nl) x;
-          (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+          (aux tm,(na,option_map (fun (_,ind,nal) -> (ind,nal)) x))) tml,
         List.map f eqnl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
       add_name found na;
       List.iter (add_name found) nal;
-      ALetTuple (nal,(na,option_app aux po),aux b,aux c)
+      ALetTuple (nal,(na,option_map aux po),aux b,aux c)
   | RIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
-      AIf (aux c,(na,option_app aux po),aux b1,aux b2)
+      AIf (aux c,(na,option_map aux po),aux b1,aux b2)
   | RCast (_,c,k,t) -> ACast (aux c,k,aux t)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
@@ -289,7 +289,7 @@ let rec subst_aconstr subst bound raw =
       and rl' = list_smartmap
         (fun (a,(n,signopt) as x) -> 
 	  let a' = subst_aconstr subst bound a in
-	  let signopt' = option_app (fun ((indkn,i),nal as z) ->
+	  let signopt' = option_map (fun ((indkn,i),nal as z) ->
 	    let indkn' = subst_kn subst indkn in
 	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
@@ -341,7 +341,7 @@ let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 (* Pattern-matching rawconstr and aconstr *)
 
 let abstract_return_type_context pi mklam tml rtno =
-  option_app (fun rtn ->
+  option_map (fun rtn ->
     let nal =
       List.flatten (List.map (fun (_,(na,t)) ->
 	match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
@@ -718,15 +718,15 @@ let map_constr_expr_with_binders f g e = function
             indnal (option_fold_right (name_fold g) na e))
 	  a e
       in
-      CCases (loc,option_app (f e') rtnpo,
+      CCases (loc,option_map (f e') rtnpo,
          List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
       let e'' = option_fold_right (name_fold g) ona e in
-      CLetTuple (loc,nal,(ona,option_app (f e'') po),f e b,f e' c)
+      CLetTuple (loc,nal,(ona,option_map (f e'') po),f e b,f e' c)
   | CIf (loc,c,(ona,po),b1,b2) ->
       let e' = option_fold_right (name_fold g) ona e in
-      CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
+      CIf (loc,f e c,(ona,option_map (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,bl,t,d) -> 
         let (e',bl') = map_local_binders f g e bl in