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, 11 insertions, 11 deletions

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 ******************************************)