Nouvelle et derniere vague de renommage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4870 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 177 insertions, 78 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9d6dd3c4f5..1fe371f855 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -163,7 +163,7 @@ let translate_v7_string dir = function
   | "add_un_Zs" -> "Psucc_Zs" (* POS_is_succ_morphism ? *)
   | "entier" -> "N"
   | "entier_of_Z" -> "Zabs_N"
-  | "Z_of_entier" -> "I_BN_Z"
+  | "Z_of_entier" -> "Z_of_N"
   | "SUPERIEUR" -> "Gt"
   | "EGAL" -> "Eq"
   | "INFERIEUR" -> "Lt"
@@ -171,7 +171,7 @@ let translate_v7_string dir = function
   | "add_carry" -> "Pplus_carry"
   | "add_assoc" -> "Pplus_assoc"
   | "add_sym" -> "Pplus_comm"
-  | "add_x_x" -> "Pplus_x_x"
+  | "add_x_x" -> "Pplus_diag"
   | "add_carry_add" -> "Pplus_carry_plus"
   | "simpl_add_r" -> "Pplus_reg_r"
   | "simpl_add_l" -> "Pplus_reg_l"
@@ -190,36 +190,38 @@ let translate_v7_string dir = function
   | "add_no_neutral" -> "Pplus_no_neutral"
   | "add_carry_not_add_un" -> "Pplus_carry_no_neutral"
   | "times" when not (is_module "Mapfold") -> "Pmult"
-  | "times_add_distr" -> "Pmult_plus_distr_r"
-  | "times_add_distr_l" -> "Pmult_plus_distr_l"
-  | "times_true_sub_distr" -> "Pmult_minus_distr_r"
+  | "times_add_distr" -> "Pmult_plus_distr_l"
+  | "times_add_distr_l" -> "Pmult_plus_distr_r"
+  | "times_true_sub_distr" -> "Pmult_minus_distr_l"
   | "times_sym" -> "Pmult_comm"
   | "times_assoc" -> "Pmult_assoc"
-  | "times_convert" -> "IPN_mult_morphism"
+  | "times_convert" -> "nat_of_P_mult_morphism"
   | "true_sub" -> "Pminus"
   | "times_x_1" -> "Pmult_1_r"
   | "times_x_double" -> "Pmult_xO_permute_r"
   | "times_x_double_plus_one" -> "Pmult_xI_permute_r"
-  | "true_sub_convert" -> "IPN_minus_morphism"
+  | "true_sub_convert" -> "nat_of_P_minus_morphism"
   | "compare_true_sub_right" -> "Pcompare_minus_r"
   | "compare_true_sub_left" -> "Pcompare_minus_l"
   | "sub_add" -> "Pplus_minus" (* similar to le_plus_minus in Arith *)
   | "sub_add_one" -> "Ppred_succ"
   | "add_sub_one" -> "Psucc_pred"
   | "add_un" -> "Psucc"
+  | "add_un_discr" -> "Psucc_discr"
   | "add_un_not_un" -> "Psucc_not_one"
   | "add_un_inj" -> "Psucc_inj"
   | "xI_add_un_xO" -> "xI_succ_xO"
-  | "ZL12" -> "Padd_one_succ_r"
-  | "ZL12bis" -> "Padd_one_succ_l"
-  | "ZL13" -> "Padd_carry_spec"
+  | "ZL12" -> "Pplus_one_succ_r"
+  | "ZL12bis" -> "Pplus_one_succ_l"
+  | "ZL13" -> "Pplus_carry_spec"
   | "ZL14" -> "Pplus_succ_permute_r"
   | "ZL14bis" -> "Pplus_succ_permute_l"
   | "sub_un" -> "Ppred"
-  | "sub_pos" -> "PminusPmask"
-  | "sub_pos_x_x" -> "PminusPmask_x_x"
-  | "sub_pos_SUPERIEUR" -> "PminusPmask_Gt"
-  | "sub_neg" -> "PminusPmask_carry"
+  | "sub_pos" -> "Pminus_mask"
+  | "sub_pos_x_x" -> "Pminus_mask_diag"
+(*  | "sub_pos_x_x" -> "Pminus_mask_diag"*)
+  | "sub_pos_SUPERIEUR" -> "Pminus_mask_Gt"
+  | "sub_neg" -> "Pminus_mask_carry"
   | "Zdiv2_pos" -> "Pdiv2"
   | "ZERO" -> "Z0"
   | "POS" -> "Zpos"
@@ -236,104 +238,138 @@ let translate_v7_string dir = function
   | "ZSH" -> "double_eq_one_discr"
   | "is_double_moins_un" -> "Psucc_double_minus_one_xO"
   | "double_moins_un_add_un_xI" -> "Pdouble_minus_one_succ_xI"
+  | "ZPminus_add_un_permute" -> "ZPminus_succ_permute"
+  | "ZPminus_add_un_permute_Zopp" -> "ZPminus_succ_permute_opp"
+  | "ZPminus_double_moins_un_xO_add_un" -> "ZPminus_double_minus_one_xO_succ"
   | "ZL1" -> "xO_succ_permute"
   | "Zplus_assoc_r" -> "Zplus_assoc_reverse"
   | "Zplus_sym" -> "Zplus_comm"
-  | "Zero_left" -> "Zplus_id_l"
-  | "Zero_right" -> "Zplus_id_r"
-  | "Zminus_n_O" -> "Zminus_id_l"
+  | "Zero_left" -> "Zplus_0_l"
+  | "Zero_right" -> "Zplus_0_r"
+  | "Zplus_n_O" -> "Zplus_0_r_reverse"
+  | "Zplus_unit_left" -> "Zplus_0_simpl_l"
+  | "Zplus_unit_right" -> "Zplus_0_simpl_l_reverse"
+  | "Zplus_Zopp_expand" -> "Zplus_opp_expand"
+  | "Zn_Sn" -> "Zsucc_discr"
+  | "Zs" -> "Zsucc"
+  | "Psucc_Zs" -> "Zpos_succ_permute"
+  | "Zs_pred" -> "Zsucc_pred"
+  | "Zpred_Sn" -> "Zpred_succ"
+  | "Zminus_n_O" -> "Zminus_0_l_reverse"
+  | "Zminus_n_n" -> "Zminus_diag_reverse"
+  | "Zminus_Sn_m" -> "Zminus_succ_l"
+  | "Zeq_Zminus" -> "Zeq_minus"
+  | "Zminus_Zeq" -> "Zminus_eq"
   | "Zplus_minus" -> "Zplus_minus_eq"
   | "Zminus_plus" -> "Zminus_plus"
-  | "Zminus_plus_simpl" -> "Zminus_plus_simpl_l_converse"
+  | "Zminus_plus_simpl" -> "Zminus_plus_simpl_l_reverse"
   | "Zminus_Zplus_compatible" -> "Zminus_plus_simpl_r"
   | "Zle_plus_minus" -> "Zplus_minus"
-  | "Zopp_Zplus" -> "Zplus_opp_distr"
+  | "Zopp_Zplus" -> "Zopp_plus_distr"
+  | "Zopp_Zopp" -> "Zopp_involutive"
+  | "Zopp_NEG" -> "Zopp_neg"
+  | "Zopp_Zdouble" -> "Zopp_double"
+  | "Zopp_Zdouble_plus_one" -> "Zopp_double_plus_one"
+  | "Zopp_Zdouble_minus_one" -> "Zopp_double_minus_one"
   | "Zplus_inverse_r" -> "Zplus_opp_r"
+  | "Zplus_inverse_l" -> "Zplus_opp_l"
+  | "Zplus_S_n" -> "Zplus_succ_l"
+  | "Zplus_n_Sm" -> "Zplus_succ_r"
+  | "Zplus_Snm_nSm" -> "Zplus_succ_comm"
   | "Zmult_assoc_r" -> "Zmult_assoc_reverse"
   | "Zmult_sym" -> "Zmult_comm"
+  | "Zmult_eq" -> "Zmult_integral_l"
+  | "Zmult_zero" -> "Zmult_integral"
   | "Zero_mult_left" -> "Zmult_0_l"
   | "Zero_mult_right" -> "Zmult_0_r"
   | "Zmult_1_n" -> "Zmult_1_l"
   | "Zmult_n_1" -> "Zmult_1_r"
-  | "Zopp_one" -> "Zopp_mult_neg_1"
-  | "Zopp_Zmult" -> "Zopp_mult_l"
-  | "Zopp_Zmult_r" -> "Zopp_mult_r_converse"
-  | "Zopp_Zmult_l" -> "Zopp_mult_l_converse"
-  | "Zmult_Zopp_left" -> "Zmult_opp_l_r"
+  | "Zmult_n_O" -> "Zmult_0_r_reverse"
+  | "Zopp_one" -> "Zopp_eq_mult_neg_1"
+  | "Zopp_Zmult" -> "Zopp_mult_distr_l_reverse"
+  | "Zopp_Zmult_r" -> "Zopp_mult_distr_r"
+  | "Zopp_Zmult_l" -> "Zopp_mult_distr_l"
+  | "Zmult_Zopp_Zopp" -> "Zmult_opp_opp"
+  | "Zmult_Zopp_left" -> "Zmult_opp_comm"
   | "Zmult_Zplus_distr" -> "Zmult_plus_distr_r"
-  | "Zmult_plus_distr" -> "Zmult_plus_distr_l"
-(*
-  | "Zmult_plus_distr_r" -> "Zmult_plus_distr_r"
-  | "Zmult_plus_distr_l" -> "Zmult_plus_distr_l"
-*)
-  | "inject_nat" -> "INZ"
-  | "inject_nat_complete" -> "INZ_complete"
-  | "inject_nat_complete_inf" -> "INZ_complete_inf"
-  | "inject_nat_prop" -> "INZ_prop"
-  | "inject_nat_set" -> "INZ_set"
-  | "convert" -> "IPN"
-  | "anti_convert" -> "INP_succ"
-  | "positive_to_nat" -> "IPN_shift"
-  | "convert_intro" -> "IPN_inj"
-  | "convert_add" -> "IPN_plus_morphism"
-  | "convert_add_un" -> "IPN_shift_succ"
-  | "convert_add_carry" -> "IPN_shift_plus_carry"
-  | "compare_convert_O" -> "lt_O_IPN"
+  | "Zmult_plus_distr" -> "Zmult_plus_distr_r"
+  | "Zmult_Zminus_distr_r" -> "Zmult_minus_distr_l"
+  | "Zmult_Zminus_distr_l" -> "Zmult_minus_distr_r"
+  | "Zcompare_Zplus_compatible" -> "Zcompare_plus_compat"
+  | "Zcompare_Zplus_compatible2" -> "Zplus_compare_compat"
+  | "Zcompare_Zmult_compatible" -> "Zcompare_mult_compat"
+  | "inject_nat" -> "Z_of_nat"
+  | "inject_nat_complete" -> "Z_of_nat_complete"
+  | "inject_nat_complete_inf" -> "Z_of_nat_complete_inf"
+  | "inject_nat_prop" -> "Z_of_nat_prop"
+  | "inject_nat_set" -> "Z_of_nat_set"
+  | "convert" -> "nat_of_P"
+  | "anti_convert" -> "P_of_succ_nat"
+  | "positive_to_nat" -> "Pmult_nat"
+  | "convert_intro" -> "nat_of_P_inj"
+  | "convert_add" -> "nat_of_P_plus_morphism"
+  | "convert_add_un" -> "Pmult_nat_succ_morphism"
+  | "cvt_add_un" -> "nat_of_P_succ_morphism"
+  | "convert_add_carry" -> "Pmult_nat_plus_carry_morphism"
+  | "compare_convert_O" -> "lt_O_nat_of_P"
   | "Zopp_intro" -> "Zopp_inj"
-  | "add_verif" -> "IPN_shift_plus_morphism"
-  | "cvt_carry" -> "IPN_plus_carry"
-  | "iter_convert" -> "iter_IPN"
+  | "plus_iter_add" -> "plus_iter_eq_plus"
+  | "add_verif" -> "Pmult_nat_plus_morphism"
+  | "ZL2" -> "Pmult_nat_shift_plus_morphism"
+  | "ZL6" -> "Pmult_nat_plus_shift_morphism"
+  | "ZL15" -> "Pplus_carry_pred_eq_plus"
+  | "cvt_carry" -> "nat_of_P_plus_carry_morphism"
+  | "iter_convert" -> "iter_nat_of_P"
   | "compare" -> "Pcompare"
   | "compare_convert1" -> "Pcompare_not_Eq"
-  | "compare_convert_INFERIEUR" -> "IPN_lt_morphism1_compare"
-  | "compare_convert_SUPERIEUR" -> "IPN_gt_morphism1_compare"
-  | "compare_convert_EGAL"      -> "compare_Eq_eq"
-  | "convert_compare_INFERIEUR" -> "IPN_lt_morphism2_compare"
-  | "convert_compare_SUPERIEUR" -> "IPN_gt_morphism2_compare"
+  | "compare_convert_INFERIEUR" -> "nat_of_P_lt_Lt_compare_morphism"
+  | "compare_convert_SUPERIEUR" -> "nat_of_P_gt_Gt_compare_morphism"
+  | "compare_convert_EGAL"      -> "Pcompare_Eq_eq"
+  | "convert_compare_INFERIEUR" -> "nat_of_P_lt_Lt_compare_complement_morphism"
+  | "convert_compare_SUPERIEUR" -> "nat_of_P_gt_Gt_compare_complement_morphism"
   | "convert_compare_EGAL"      -> "Pcompare_refl"
   | "Zcompare_EGAL"             -> "Zcompare_Eq_iff_eq"
   | "Zcompare_EGAL_eq"          -> "Zcompare_Eq_eq"
   | "Zcompare_x_x"              -> "Zcompare_refl"
   | "Zcompare_et_un"            -> "Zcompare_Gt_not_Lt"
   | "Zcompare_trans_SUPERIEUR"  -> "Zcompare_Gt_trans"
-  | "Zcompare_n_S"              -> "Zcompare_Zs_compatible"
+  | "Zcompare_n_S"              -> "Zcompare_succ_compat"
   | "SUPERIEUR_POS"             -> "Zcompare_Gt_spec"
   | "Zcompare_ANTISYM"          -> "Zcompare_antisym"
-  | "compare_positive_to_nat_O" -> "le_IPN_shift"
-  | "Zcompare_Zs_SUPERIEUR"     -> "Zcompare_Zs_Gt"
+  | "compare_positive_to_nat_O" -> "le_Pmult_nat"
+  | "Zcompare_Zs_SUPERIEUR"     -> "Zcompare_succ_Gt"
+  | "Zcompare_Zopp"             -> "Zcompare_opp"
   | "ZLSI" -> "Pcompare_Gt_Lt"
   | "ZLIS" -> "Pcompare_Lt_Gt"
   | "ZLII" -> "Pcompare_Lt_Lt"
   | "ZLSS" -> "Pcompare_Gt_Gt"
-  | "bij1" -> "IPN_INP_succ_eq_succ"
-  | "bij2" -> "INP_succ_IPN_eq_succ"
-  | "bij3" -> "pred_INP_succ_IPN_bij"
-  | "POS_inject" -> "Zpos_eq_INZ_IPN"
+  | "bij1" -> "nat_of_P_o_P_of_succ_nat_eq_succ"
+  | "bij2" -> "P_of_succ_nat_o_nat_of_P_eq_succ"
+  | "bij3" -> "pred_o_P_of_succ_nat_o_nat_of_P_eq_id"
+  | "POS_inject" -> "Zpos_eq_Z_of_nat_o_nat_of_P"
   | "absolu" -> "Zabs_nat"
   | "absolu_lt" -> "Zabs_nat_lt" (* "Zabs_nat_lt_morphism_pos" ? *)
-  | "Zeq_add_S" -> "Zs_inj"
-  | "Znot_eq_S" -> "Zs_inj_contrapositive"
-  | "Zeq_S" -> "Zs_eq_compat"
-  | "Zs_pred" -> "Zs_pred"
-  | "Zpred_Sn" -> "Zpred_Zs"
+  | "Zeq_add_S" -> "Zsucc_inj"
+  | "Znot_eq_S" -> "Zsucc_inj_contrapositive"
+  | "Zeq_S" -> "Zsucc_eq_compat"
   | "Zsimpl_plus_l" -> "Zplus_reg_l"
   | "Zplus_simpl" -> "Zplus_eq_compat"
-  | "POS_gt_ZERO" -> "Zpos_gt_0"
-  | "ZERO_le_POS" -> "Z0_le_pos"
-  | "NEG_lt_ZERO" -> "Zneg_lt_0"
-  | "Zlt_ZERO_pred_le_ZERO" -> "Zlt_0_pred_le_0"
+  | "POS_gt_ZERO" -> "Zgt_pos_0"
+  | "ZERO_le_POS" -> "Zle_0_pos"
+  | "ZERO_le_inj" -> "Zle_0_nat"
+  | "NEG_lt_ZERO" -> "Zlt_neg_0"
+  | "Zlt_ZERO_pred_le_ZERO" -> "Zlt_0_le_0_pred"
   | "POS_xI" -> "Zpos_xI"
   | "POS_xO" -> "Zpos_xO"
   | "NEG_xI" -> "Zneg_xI"
   | "NEG_xO" -> "Zneg_xO"
-  | "POS_add" -> "Zpos_plus"
-  | "NEG_add" -> "Zneg_plus"
+  | "POS_add" -> "Zpos_plus_distr"
+  | "NEG_add" -> "Zneg_plus_distr"
   (* Z Orders *)
   | "not_Zge" -> "Znot_ge_lt"
   | "not_Zlt" -> "Znot_lt_ge"
   | "not_Zle" -> "Znot_le_gt"
   | "not_Zgt" -> "Znot_gt_le"
-
   | "Zgt_not_sym" -> "Zgt_asym"
   | "Zlt_not_sym" -> "Zlt_asym"
   | "Zlt_n_n" -> "Zlt_irrefl"
@@ -361,11 +397,18 @@ let translate_v7_string dir = function
   | "Zlt_Zmult_right2" -> "Zmult_gt_0_lt_reg_r"
   | "Zlt_Zmult_right" -> "Zmult_gt_0_lt_compat_r"
   | "Zle_Zmult_right2" -> "Zmult_gt_0_le_reg_r"
-  | "Zle_Zmult_right" -> "Zmult_ge_0_le_compat_r"
+  | "Zle_Zmult_right" -> "Zmult_gt_0_le_compat_r"
   | "Zgt_Zmult_right" -> "Zmult_gt_compat_r"
   | "Zgt_Zmult_left" -> "Zmult_gt_compat_l"
   | "Zlt_Zmult_left" -> "Zmult_gt_0_lt_compat_l"
+  | "Zcompare_Zmult_right" -> "Zmult_compare_compat_r"
+  | "Zcompare_Zmult_left" -> "Zmult_compare_compat_l"
+  | "Zplus_Zmult_2" -> "Zplus_diag_eq_mult_2"
+  | "Zmult_Sm_n" -> "Zmult_succ_l_reverse"
+  | "Zmult_n_Sm" -> "Zmult_succ_r_reverse"
   | "Zmult_le" -> "Zmult_le_0_reg_r"
+  | "Zmult_reg_left" -> "Zmult_reg_l"
+  | "Zmult_reg_right" -> "Zmult_reg_r"
   | "Zle_ZERO_mult" -> "Zmult_le_0_compat"
   | "Zgt_ZERO_mult" -> "Zmult_gt_0_compat"
   | "Zle_mult" -> "Zmult_gt_0_le_0_compat"
@@ -376,18 +419,55 @@ let translate_v7_string dir = function
   | "Zge_Zmult_pos_right" -> "Zmult_ge_compat_r"
   | "Zge_Zmult_pos_left" -> "Zmult_ge_compat_l"
   | "Zge_Zmult_pos_compat" -> "Zmult_ge_compat"
+  | "Zlt_Zcompare" -> "Zlt_compare"
+  | "Zle_Zcompare" -> "Zle_compare"
+  | "Zgt_Zcompare" -> "Zgt_compare"
+  | "Zge_Zcompare" -> "Zge_compare"
   (* IntMap *)
-  | "convert_xH" -> "IPN_xH"
-  | "convert_xO" -> "IPN_xO"
-  | "convert_xI" -> "IPN_xI"
-  | "positive_to_nat_mult" -> "IPN_shift_mult"
-  | "positive_to_nat_2" -> "IPN_shift_2"
-  | "positive_to_nat_4" -> "IPN_shift_4"
+  | "convert_xH" -> "nat_of_P_xH"
+  | "convert_xO" -> "nat_of_P_xO"
+  | "convert_xI" -> "nat_of_P_xI"
+  | "positive_to_nat_mult" -> "Pmult_nat_mult_permute"
+  | "positive_to_nat_2" -> "Pmult_nat_2_mult_2_permute"
+  | "positive_to_nat_4" -> "Pmult_nat_4_mult_2_permute"
   (* ZArith and Arith orders *)
   | "Zle_refl" -> "Zeq_le"
-  | "Zle_trans_S" -> "Zle_Sn_le"
+  | "Zle_n" -> "Zle_refl"
+  | "Zle_trans_S" -> "Zle_succ_le"
+  | "Zgt_trans_S" -> "Zge_trans_succ"
+  | "Zgt_S" -> "Zgt_succ_gt_or_eq"
+  | "Zle_Sn_n" -> "Znot_le_succ"
+  | "Zlt_n_Sn" -> "Zlt_succ"
+  | "Zlt_S" -> "Zlt_lt_succ"
+  | "Zlt_n_S" -> "Zsucc_lt_compat"
+  | "Zle_n_S" -> "Zsucc_le_compat"
+  | "Zgt_n_S" -> "Zsucc_gt_compat"
+  | "Zlt_S_n" -> "Zsucc_lt_reg"
+  | "Zgt_S_n" -> "Zsucc_gt_reg"
+  | "Zle_S_n" -> "Zsucc_le_reg"
+  | "Zle_0_plus" -> "Zplus_le_0_compat"
+  | "Zgt_Sn_n" -> "Zgt_succ"
+  | "Zgt_le_S" -> "Zgt_le_succ"
+  | "Zgt_S_le" -> "Zgt_succ_le"
+  | "Zle_S_gt" -> "Zlt_succ_gt"
+  | "Zle_gt_S" -> "Zlt_gt_succ"
+  | "Zgt_pred" -> "Zgt_succ_pred"
+  | "Zlt_pred" -> "Zlt_succ_pred"
+  | "Zgt0_le_pred" -> "Zgt_0_le_0_pred"
+  | "Z_O_1" -> "Zlt_0_1"
+  | "Zle_NEG_POS" -> "Zle_neg_pos"
+  | "Zle_n_Sn" -> "Zle_succ"
+  | "Zle_pred_n" -> "Zle_pred"
+  | "Zlt_pred_n_n" -> "Zlt_pred"
+  | "Zlt_le_S" -> "Zlt_le_succ"
+  | "Zlt_n_Sm_le" -> "Zlt_succ_le"
+  | "Zle_lt_n_Sm" -> "Zle_lt_succ"
+  | "Zle_le_S" -> "Zle_le_succ"
+  | "Zlt_minus" -> "Zlt_minus_simpl_swap"
   | "le_trans_S" -> "le_Sn_le"
   (* Arith *)
+  | "plus_n_O" -> "plus_0_r_reverse"
+  | "plus_O_n" -> "plus_0_l"
   | "plus_assoc_l" -> "plus_assoc"
   | "plus_assoc_r" -> "plus_assoc_reverse"
   | "plus_sym" -> "plus_comm"
@@ -398,13 +478,19 @@ let translate_v7_string dir = function
   | "lt_not_sym" -> "lt_asym"
   | "gt_antirefl" -> "gt_irrefl"
   | "lt_n_n" -> "lt_irrefl"
+(* Trop utilisé dans CoqBook | "le_n" -> "le_refl"*)
   | "simpl_plus_l" -> "plus_reg_l"
   | "simpl_plus_r" -> "plus_reg_r"
   | "fact_growing" -> "fact_le"
   | "mult_assoc_l" -> "mult_assoc"
   | "mult_assoc_r" -> "mult_assoc_reverse"
+  | "mult_plus_distr" -> "mult_plus_distr_r"
+  | "mult_plus_distr_r" -> "mult_plus_distr_l"
+  | "mult_minus_distr" -> "mult_minus_distr_r"
   | "mult_1_n" -> "mult_1_l"
   | "mult_n_1" -> "mult_1_r"
+  | "mult_n_O" -> "mult_O_r_reverse"
+  | "mult_n_Sm" -> "mult_S_r_reverse"
   | "lt_mult_left" -> "mult_S_lt_compat_l"
   | "mult_le" -> "mult_le_compat_l"
   | "le_mult_right" -> "mult_le_compat_r"
@@ -416,6 +502,8 @@ let translate_v7_string dir = function
   | "IHexists" -> "IHexists_between"
   | "pred_Sn" -> "pred_S"
   | "inj_minus_aux" -> "not_le_minus_0"
+  | "minus_x_x" -> "minus_diag"
+  | "minus_plus_simpl" -> "minus_plus_simpl_l_reverse"
   | "gt_reg_l" -> "plus_gt_compat_l"
   | "le_reg_l" -> "plus_le_compat_l"
   | "le_reg_r" -> "plus_le_compat_r"
@@ -429,13 +517,24 @@ let translate_v7_string dir = function
   | "simpl_gt_plus_l" -> "plus_gt_reg_l"
   | "simpl_le_plus_l" -> "plus_le_reg_l"
   | "simpl_lt_plus_l" -> "plus_lt_reg_l"
+(* Noms sur le principe de ceux de Z
+  | "le_n_S" -> "S_le_compat"
+  | "le_n_Sn" -> "le_S"
+(*  | "le_O_n" -> "??" *)
+  | "le_pred_n" -> "le_pred"
+  | "le_trans_S" -> "le_S_le"
+  | "le_S_n" -> "S_le_reg"
+  | "le_Sn_O" -> "not_le_S_O"
+  | "le_Sn_n" -> "not_le_S"
+*)
   (* Init *)
+  | "IF" -> "IF_then_else"
   | "relation" when is_module "Datatypes" or is_dir dir "Datatypes"
       -> "comparison"
   | "Op" when is_module "Datatypes" or is_dir dir "Datatypes"
       -> "CompOpp"
   (* Lists *)
-  | "idempot_rev" -> "involutive_rev"
+  | "idempot_rev" -> "rev_involutive"
   | "forall" -> "HereAndFurther"
   (* Bool *)
   | "orb_sym" -> "orb_comm"