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

7 files changed, 58 insertions, 58 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index edda5c25b9..f7ae4311c7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -778,7 +778,7 @@ let gen_auto n lems dbnames =
   | None -> full_auto n lems
   | Some l -> auto n lems l
 
-let inj_or_var = option_app (fun n -> Genarg.ArgArg n)
+let inj_or_var = option_map (fun n -> Genarg.ArgArg n)
 
 let h_auto n lems l =
   Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index bea6f33037..598a6fe0ae 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -107,7 +107,7 @@ let e_split = e_constructor_tac (Some 1) 1
 TACTIC EXTEND econstructor
   [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ]
 | [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ]
-| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_app Tacinterp.eval_tactic t) ] 
+| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_map Tacinterp.eval_tactic t) ] 
       END
 
 TACTIC EXTEND eleft
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 97aeedc6b3..1c0e04276e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -80,7 +80,7 @@ END
 
 TACTIC EXTEND replace 
 | ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp)  by_arg_tac(tac)  ] ->
-    [ new_replace c1 c2 in_hyp (Util.option_app Tacinterp.eval_tactic tac)  ]
+    [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac)  ]
 END
 
 (* Julien:
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 73259b5ffa..e0fd138c2b 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -23,7 +23,7 @@ let inj_id id = (dummy_loc,id)
 
 (* Basic tactics *)
 let h_intro_move x y =
-  abstract_tactic (TacIntroMove (x, option_app inj_id y)) (intro_move x y)
+  abstract_tactic (TacIntroMove (x, option_map inj_id y)) (intro_move x y)
 let h_intro x        = h_intro_move (Some x) None
 let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
 let h_assumption     = abstract_tactic TacAssumption assumption
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index cb042d4256..d53ca6126e 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -43,14 +43,14 @@ let get_dn dnm hkey =
   try Gmap.find hkey dnm with Not_found -> Btermdn.create ()
 
 let add dn (na,(pat,valu)) =
-  let hkey = option_app fst (Termdn.constr_pat_discr pat) in 
+  let hkey = option_map fst (Termdn.constr_pat_discr pat) in 
   dn.table <- Gmap.add na (pat,valu) dn.table;
   let dnm = dn.patterns in
   dn.patterns <- Gmap.add hkey (Btermdn.add (get_dn dnm hkey) (pat,valu)) dnm
     
 let rmv dn na =
   let (pat,valu) = Gmap.find na dn.table in
-  let hkey = option_app fst (Termdn.constr_pat_discr pat) in 
+  let hkey = option_map fst (Termdn.constr_pat_discr pat) in 
   dn.table <- Gmap.remove na dn.table;
   let dnm = dn.patterns in
   dn.patterns <- Gmap.add hkey (Btermdn.rmv (get_dn dnm hkey) (pat,valu)) dnm
@@ -62,7 +62,7 @@ let remap ndn na (pat,valu) =
   add ndn (na,(pat,valu))
 
 let lookup dn valu =
-  let hkey = option_app fst (Termdn.constr_val_discr valu) in 
+  let hkey = option_map fst (Termdn.constr_val_discr valu) in 
   try Btermdn.lookup (Gmap.find hkey  dn.patterns) valu with Not_found -> []
 
 let app f dn = Gmap.iter f dn.table
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 83f7f39bb4..7b4c5b8dba 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -85,7 +85,7 @@ type morphism_class =
 let subst_mps_in_relation_class subst =
  function
     Relation  t -> Relation  (subst_mps subst t)
-  | Leibniz t -> Leibniz (option_app (subst_mps subst) t) 
+  | Leibniz t -> Leibniz (option_map (subst_mps subst) t) 
 
 let subst_mps_in_argument_class subst (variance,rel) =
  variance, subst_mps_in_relation_class subst rel
@@ -295,9 +295,9 @@ let relation_morphism_of_constr_morphism =
 let subst_relation subst relation = 
   let rel_a' = subst_mps subst relation.rel_a in
   let rel_aeq' = subst_mps subst relation.rel_aeq in
-  let rel_refl' = option_app (subst_mps subst) relation.rel_refl in
-  let rel_sym' = option_app (subst_mps subst) relation.rel_sym in
-  let rel_trans' = option_app (subst_mps subst) relation.rel_trans in
+  let rel_refl' = option_map (subst_mps subst) relation.rel_refl in
+  let rel_sym' = option_map (subst_mps subst) relation.rel_sym in
+  let rel_trans' = option_map (subst_mps subst) relation.rel_trans in
   let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in
   let rel_Xreflexive_relation_class' =
    subst_mps subst relation.rel_Xreflexive_relation_class
@@ -638,9 +638,9 @@ let apply_to_relation subst rel =
    assert (new_quantifiers_no >= 0) ;
    { rel_a = mkApp (rel.rel_a, subst) ;
      rel_aeq = mkApp (rel.rel_aeq, subst) ;
-     rel_refl = option_app (fun c -> mkApp (c,subst)) rel.rel_refl ; 
-     rel_sym = option_app (fun c -> mkApp (c,subst)) rel.rel_sym;
-     rel_trans = option_app (fun c -> mkApp (c,subst)) rel.rel_trans;
+     rel_refl = option_map (fun c -> mkApp (c,subst)) rel.rel_refl ; 
+     rel_sym = option_map (fun c -> mkApp (c,subst)) rel.rel_sym;
+     rel_trans = option_map (fun c -> mkApp (c,subst)) rel.rel_trans;
      rel_quantifiers_no = new_quantifiers_no;
      rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst);
      rel_Xreflexive_relation_class =
@@ -1078,9 +1078,9 @@ let int_add_relation id a aeq refl sym trans =
       let a_instance = apply_to_rels a a_quantifiers_rev in
       let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
       let sym_instance =
-       option_app (fun x -> apply_to_rels x a_quantifiers_rev) sym in
+       option_map (fun x -> apply_to_rels x a_quantifiers_rev) sym in
       let refl_instance =
-       option_app (fun x -> apply_to_rels x a_quantifiers_rev) refl in
+       option_map (fun x -> apply_to_rels x a_quantifiers_rev) refl in
       let trans_instance = apply_to_rels trans a_quantifiers_rev in
       let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output =
        match sym_instance, refl_instance with
@@ -1134,8 +1134,8 @@ let int_add_relation id a aeq refl sym trans =
 
 (* The vernac command "Add Relation ..." *)
 let add_relation id a aeq refl sym trans =
- int_add_relation id (constr_of a) (constr_of aeq) (option_app constr_of refl)
-  (option_app constr_of sym) (option_app constr_of trans)
+ int_add_relation id (constr_of a) (constr_of aeq) (option_map constr_of refl)
+  (option_map constr_of sym) (option_map constr_of trans)
 
 (************************ Add Setoid ******************************************)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f24297cf05..2eb2d88f4d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -514,7 +514,7 @@ let intern_redexp ist = function
   | Cbv f -> Cbv (intern_flag ist f)
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l)
-  | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o)
+  | Simpl o -> Simpl (option_map (intern_constr_occurrence ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
   
 
@@ -523,7 +523,7 @@ let intern_inversion_strength lf ist = function
       NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
       intern_intro_pattern lf ist ids)
   | DepInversion (k,copt,ids) ->
-      DepInversion (k, option_app (intern_constr ist) copt,
+      DepInversion (k, option_map (intern_constr ist) copt,
       intern_intro_pattern lf ist ids)
   | InversionUsing (c,idl) ->
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
@@ -618,29 +618,29 @@ let rec intern_atomic lf ist x =
       TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
   | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
-      TacIntroMove (option_app (intern_ident lf ist) ido,
-          option_app (intern_hyp ist) ido')
+      TacIntroMove (option_map (intern_ident lf ist) ido,
+          option_map (intern_hyp ist) ido')
   | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (intern_constr ist c)
   | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
   | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
   | TacElim (cb,cbo) ->
       TacElim (intern_constr_with_bindings ist cb,
-               option_app (intern_constr_with_bindings ist) cbo)
+               option_map (intern_constr_with_bindings ist) cbo)
   | TacElimType c -> TacElimType (intern_type ist c)
   | TacCase cb -> TacCase (intern_constr_with_bindings ist cb)
   | TacCaseType c -> TacCaseType (intern_type ist c)
-  | TacFix (idopt,n) -> TacFix (option_app (intern_ident lf ist) idopt,n)
+  | TacFix (idopt,n) -> TacFix (option_map (intern_ident lf ist) idopt,n)
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
       TacMutualFix (intern_ident lf ist id, n, List.map f l)
-  | TacCofix idopt -> TacCofix (option_app (intern_ident lf ist) idopt)
+  | TacCofix idopt -> TacCofix (option_map (intern_ident lf ist) idopt)
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
-      TacAssert (option_app (intern_tactic ist) otac,
+      TacAssert (option_map (intern_tactic ist) otac,
                  intern_intro_pattern lf ist ipat,
                  intern_constr_gen (otac<>None) ist c)
   | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
@@ -660,26 +660,26 @@ let rec intern_atomic lf ist x =
   (* Automation tactics *)
   | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
   | TacAuto (n,lems,l) ->
-      TacAuto (option_app (intern_int_or_var ist) n,
+      TacAuto (option_map (intern_int_or_var ist) n,
         List.map (intern_constr ist) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
-  | TacDAuto (n,p) -> TacDAuto (option_app (intern_int_or_var ist) n,p)
+  | TacDAuto (n,p) -> TacDAuto (option_map (intern_int_or_var ist) n,p)
 
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       TacSimpleInduction (intern_quantified_hypothesis ist h)
   | TacNewInduction (lc,cbo,ids) ->
       TacNewInduction (List.map (intern_induction_arg ist) lc,
-               option_app (intern_constr_with_bindings ist) cbo,
+               option_map (intern_constr_with_bindings ist) cbo,
                (intern_intro_pattern lf ist ids))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (List.map (intern_induction_arg ist) c,
-               option_app (intern_constr_with_bindings ist) cbo,
+               option_map (intern_constr_with_bindings ist) cbo,
 	       (intern_intro_pattern lf ist ids))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
@@ -703,14 +703,14 @@ let rec intern_atomic lf ist x =
   | TacLeft bl -> TacLeft (intern_bindings ist bl)
   | TacRight bl -> TacRight (intern_bindings ist bl)
   | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl)
-  | TacAnyConstructor t -> TacAnyConstructor (option_app (intern_tactic ist) t)
+  | TacAnyConstructor t -> TacAnyConstructor (option_map (intern_tactic ist) t)
   | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
       TacReduce (intern_redexp ist r, clause_app (intern_hyp_location ist) cl)
   | TacChange (occl,c,cl) ->
-      TacChange (option_app (intern_constr_occurrence ist) occl,
+      TacChange (option_map (intern_constr_occurrence ist) occl,
         intern_constr ist c, clause_app (intern_hyp_location ist) cl)
 
   (* Equivalence relations *)
@@ -750,7 +750,7 @@ and intern_tactic_seq ist = function
   | TacLetIn (l,u) ->
       let l = List.map
         (fun (n,c,b) ->
-          (n,option_app (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
+          (n,option_map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
       let (l1,l2) = ist.ltacvars in
       let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
       ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
@@ -1124,7 +1124,7 @@ let interp_evaluable ist env = function
 let interp_hyp_location ist gl (id,occs,hl) = (interp_hyp ist gl id,occs,hl)
 
 let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
-  { onhyps=option_app(List.map (interp_hyp_location ist gl)) ol;
+  { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol;
     onconcl=b;
     concl_occs=occs }
 
@@ -1271,7 +1271,7 @@ let redexp_interp ist sigma env = function
   | Cbv f -> Cbv (interp_flag ist env f)
   | Lazy f -> Lazy (interp_flag ist env f)
   | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
-  | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o)
+  | Simpl o -> Simpl (option_map (interp_pattern ist sigma env) o)
   | (Red _ |  Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
@@ -1719,23 +1719,23 @@ and interp_atomic ist gl = function
   | TacIntrosUntil hyp ->
       h_intros_until (interp_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
-      h_intro_move (option_app (interp_ident ist) ido)
-      (option_app (interp_hyp ist gl) ido')
+      h_intro_move (option_map (interp_ident ist) ido)
+      (option_map (interp_hyp ist gl) ido')
   | TacAssumption -> h_assumption
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
   | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
   | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
   | TacElim (cb,cbo) ->
       h_elim (interp_constr_with_bindings ist gl cb)
-                (option_app (interp_constr_with_bindings ist gl) cbo)
+                (option_map (interp_constr_with_bindings ist gl) cbo)
   | TacElimType c -> h_elim_type (pf_interp_type ist gl c)
   | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb)
   | TacCaseType c -> h_case_type (pf_interp_type ist gl c)
-  | TacFix (idopt,n) -> h_fix (option_app (interp_ident ist) idopt) n
+  | TacFix (idopt,n) -> h_fix (option_map (interp_ident ist) idopt) n
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (interp_ident ist id,n,pf_interp_type ist gl c) in
       h_mutual_fix (interp_ident ist id) n (List.map f l)
-  | TacCofix idopt -> h_cofix (option_app (interp_ident ist) idopt)
+  | TacCofix idopt -> h_cofix (option_map (interp_ident ist) idopt)
   | TacMutualCofix (id,l) ->
       let f (id,c) = (interp_ident ist id,pf_interp_type ist gl c) in
       h_mutual_cofix (interp_ident ist id) (List.map f l)
@@ -1743,7 +1743,7 @@ and interp_atomic ist gl = function
   | TacAssert (t,ipat,c) ->
       let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
       abstract_tactic (TacAssert (t,ipat,c))
-        (Tactics.forward (option_app (interp_tactic ist) t)
+        (Tactics.forward (option_map (interp_tactic ist) t)
 	  (interp_intro_pattern ist ipat) c)
   | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
@@ -1760,29 +1760,29 @@ and interp_atomic ist gl = function
   (* Automation tactics *)
   | TacTrivial (lems,l) -> 
       Auto.h_trivial (List.map (pf_interp_constr ist gl) lems)
-	(option_app (List.map (interp_hint_base ist)) l)
+	(option_map (List.map (interp_hint_base ist)) l)
   | TacAuto (n,lems,l) ->
-      Auto.h_auto (option_app (interp_int_or_var ist) n)
+      Auto.h_auto (option_map (interp_int_or_var ist) n)
       (List.map (pf_interp_constr ist gl) lems)
-      (option_app (List.map (interp_hint_base ist)) l)
+      (option_map (List.map (interp_hint_base ist)) l)
   | TacAutoTDB n -> Dhyp.h_auto_tdb n
   | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
   | TacDestructConcl -> Dhyp.h_destructConcl
   | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
-  | TacDAuto (n,p) -> Auto.h_dauto (option_app (interp_int_or_var ist) n,p)
+  | TacDAuto (n,p) -> Auto.h_dauto (option_map (interp_int_or_var ist) n,p)
 
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       h_simple_induction (interp_quantified_hypothesis ist h)
   | TacNewInduction (lc,cbo,ids) ->
       h_new_induction (List.map (interp_induction_arg ist gl) lc)
-        (option_app (interp_constr_with_bindings ist gl) cbo)
+        (option_map (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist ids)
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (List.map (interp_induction_arg ist gl) c)
-        (option_app (interp_constr_with_bindings ist gl) cbo)
+        (option_map (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
@@ -1811,7 +1811,7 @@ and interp_atomic ist gl = function
   | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl)
   | TacAnyConstructor t ->
       abstract_tactic (TacAnyConstructor t)
-        (Tactics.any_constructor (option_app (interp_tactic ist) t))
+        (Tactics.any_constructor (option_map (interp_tactic ist) t))
   | TacConstructor (n,bl) ->
       h_constructor (skip_metaid n) (interp_bindings ist gl bl)
 
@@ -1819,7 +1819,7 @@ and interp_atomic ist gl = function
   | TacReduce (r,cl) ->
       h_reduce (pf_redexp_interp ist gl r) (interp_clause ist gl cl)
   | TacChange (occl,c,cl) ->
-      h_change (option_app (pf_interp_pattern ist gl) occl)
+      h_change (option_map (pf_interp_pattern ist gl) occl)
         (pf_interp_constr ist gl c) (interp_clause ist gl cl)
 
   (* Equivalence relations *)
@@ -1829,7 +1829,7 @@ and interp_atomic ist gl = function
 
   (* Equality and inversion *)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
-      Inv.dinv k (option_app (pf_interp_constr ist gl) c)
+      Inv.dinv k (option_map (pf_interp_constr ist gl) c)
         (interp_intro_pattern ist ids)
         (interp_declared_or_quantified_hypothesis ist gl hyp)
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
@@ -1977,7 +1977,7 @@ let subst_redexp subst = function
   | Cbv f -> Cbv (subst_flag subst f)
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
-  | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o)
+  | Simpl o -> Simpl (option_map (subst_constr_occurrence subst) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let subst_raw_may_eval subst = function
@@ -2005,7 +2005,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
   | TacElim (cb,cbo) ->
       TacElim (subst_raw_with_bindings subst cb,
-               option_app (subst_raw_with_bindings subst) cbo)
+               option_map (subst_raw_with_bindings subst) cbo)
   | TacElimType c -> TacElimType (subst_rawconstr subst c)
   | TacCase cb -> TacCase (subst_raw_with_bindings subst cb)
   | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
@@ -2035,11 +2035,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacSimpleInduction h as x -> x
   | TacNewInduction (lc,cbo,ids) -> (* Pierre C. est-ce correct? *)
       TacNewInduction (List.map (subst_induction_arg subst) lc,
-               option_app (subst_raw_with_bindings subst) cbo, ids)
+               option_map (subst_raw_with_bindings subst) cbo, ids)
   | TacSimpleDestruct h as x -> x
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (List.map (subst_induction_arg subst) c,  (* Julien F. est-ce correct? *)
-               option_app (subst_raw_with_bindings subst) cbo, ids)
+               option_map (subst_raw_with_bindings subst) cbo, ids)
   | TacDoubleInduction (h1,h2) as x -> x
   | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
   | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
@@ -2059,13 +2059,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacLeft bl -> TacLeft (subst_bindings subst bl)
   | TacRight bl -> TacRight (subst_bindings subst bl)
   | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl)
-  | TacAnyConstructor t -> TacAnyConstructor (option_app (subst_tactic subst) t)
+  | TacAnyConstructor t -> TacAnyConstructor (option_map (subst_tactic subst) t)
   | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl)
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (occl,c,cl) ->
-      TacChange (option_app (subst_constr_occurrence subst) occl,
+      TacChange (option_map (subst_constr_occurrence subst) occl,
         subst_rawconstr subst c, cl)
 
   (* Equivalence relations *)
@@ -2074,7 +2074,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 
   (* Equality and inversion *)
   | TacInversion (DepInversion (k,c,l),hyp) ->
-     TacInversion (DepInversion (k,option_app (subst_rawconstr subst) c,l),hyp)
+     TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp)
   | TacInversion (NonDepInversion _,_) as x -> x
   | TacInversion (InversionUsing (c,cl),hyp) ->
       TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp)
@@ -2093,7 +2093,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
       TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
   | TacLetIn (l,u) ->
-      let l = List.map (fun (n,c,b) -> (n,option_app (subst_tactic subst) c,subst_tacarg subst b)) l in
+      let l = List.map (fun (n,c,b) -> (n,option_map (subst_tactic subst) c,subst_tacarg subst b)) l in
       TacLetIn (l,subst_tactic subst u)
   | TacMatchContext (lz,lr,lmr) ->
       TacMatchContext(lz,lr, subst_match_rule subst lmr)