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

1 files changed, 40 insertions, 40 deletions

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)