Nouvelle vague de renommage

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

1 files changed, 46 insertions, 5 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 461eabf59..338457668 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -185,6 +185,7 @@ let translate_v7_string dir = function
   | "double_moins_un_plus_xO_double_moins_un" ->
       "Pdouble_minus_one_plus_xO_double_minus_one"
   | "add_xI_double_moins_un" -> "Pplus_xI_double_minus_one"
+  | "add_xO_double_moins_un" -> "Pplus_xO_double_minus_one"
   | "iter_pos_add" -> "iter_pos_plus"
   | "add_no_neutral" -> "Pplus_no_neutral"
   | "add_carry_not_add_un" -> "Pplus_carry_no_neutral"
@@ -236,6 +237,7 @@ let translate_v7_string dir = function
   | "is_double_moins_un" -> "Psucc_double_minus_one_xO"
   | "double_moins_un_add_un_xI" -> "Pdouble_minus_one_succ_xI"
   | "ZL1" -> "xO_succ_permute"
+  | "Zplus_assoc_r" -> "Zplus_assoc_reverse"
   | "Zplus_sym" -> "Zplus_comm"
   | "Zero_left" -> "Zplus_id_l"
   | "Zero_right" -> "Zplus_id_r"
@@ -247,6 +249,7 @@ let translate_v7_string dir = function
   | "Zle_plus_minus" -> "Zplus_minus"
   | "Zopp_Zplus" -> "Zplus_opp_distr"
   | "Zplus_inverse_r" -> "Zplus_opp_r"
+  | "Zmult_assoc_r" -> "Zmult_assoc_reverse"
   | "Zmult_sym" -> "Zmult_comm"
   | "Zero_mult_left" -> "Zmult_0_l"
   | "Zero_mult_right" -> "Zmult_0_r"
@@ -257,8 +260,12 @@ let translate_v7_string dir = function
   | "Zopp_Zmult_r" -> "Zopp_mult_r_converse"
   | "Zopp_Zmult_l" -> "Zopp_mult_l_converse"
   | "Zmult_Zopp_left" -> "Zmult_opp_l_r"
+  | "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"
@@ -321,6 +328,11 @@ let translate_v7_string dir = function
   | "POS_add" -> "Zpos_plus"
   | "NEG_add" -> "Zneg_plus"
   (* 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"
@@ -333,6 +345,9 @@ let translate_v7_string dir = function
   | "Zle_reg_r" -> "Zplus_le_compat_r"
   | "Zlt_le_reg" -> "Zplus_lt_le_compat"
   | "Zle_lt_reg" -> "Zplus_le_lt_compat"
+  | "Zle_plus_plus" -> "Zplus_le_compat"
+  | "Zlt_Zplus" -> "Zplus_lt_compat"
+  | "Zle_O_plus" -> "Zplus_le_0_compat"
   | "Zle_mult_simpl" -> "Zmult_le_reg_r"
   | "Zge_mult_simpl" -> "Zmult_ge_reg_r"
   | "Zgt_mult_simpl" -> "Zmult_gt_reg_r"
@@ -342,8 +357,24 @@ let translate_v7_string dir = function
   | "Zsimpl_le_plus_r" -> "Zplus_le_reg_r"
   | "Zsimpl_lt_plus_l" -> "Zplus_lt_reg_l"
   | "Zsimpl_lt_plus_r" -> "Zplus_lt_reg_r"
-  | "Zlt_Zmult_left"  -> "Zmult_lt_compat_l"
-  | "Zlt_Zmult_right" -> "Zmult_lt_compat_r"
+  | "Zlt_Zmult_right2" -> "Zmult_lt_reg_r"
+  | "Zlt_Zmult_right" -> "Zmult_gt_0_lt_compat_r"
+  | "Zle_Zmult_right2" -> "Zmult_le_reg_r"
+  | "Zle_Zmult_right" -> "Zmult_ge_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"
+  | "Zmult_le" -> "Zmult_le_0_reg_r"
+  | "Zle_ZERO_mult" -> "Zmult_le_0_compat"
+  | "Zgt_ZERO_mult" -> "Zmult_gt_0_compat"
+  | "Zle_mult" -> "Zmult_gt_0_le_0_compat"
+  | "Zmult_lt" -> "Zmult_gt_0_lt_0_reg_r"
+  | "Zmult_gt" -> "Zmult_gt_0_reg_l"
+  | "Zle_Zmult_pos_right" -> "Zmult_le_compat_r"
+  | "Zle_Zmult_pos_left" -> "Zmult_le_compat_l"
+  | "Zge_Zmult_pos_right" -> "Zmult_ge_compat_r"
+  | "Zge_Zmult_pos_left" -> "Zmult_ge_compat_l"
+  | "Zge_Zmult_pos_compat" -> "Zmult_ge_compat"
   (* IntMap *)
   | "convert_xH" -> "IPN_xH"
   | "convert_xO" -> "IPN_xO"
@@ -356,6 +387,8 @@ let translate_v7_string dir = function
   | "Zle_trans_S" -> "Zle_Sn_le"
   | "le_trans_S" -> "le_Sn_le"
   (* Arith *)
+  | "plus_assoc_l" -> "plus_assoc"
+  | "plus_assoc_r" -> "plus_assoc_reverse"
   | "plus_sym" -> "plus_comm"
   | "mult_sym" -> "mult_comm"
   | "max_sym" -> "max_comm"
@@ -367,9 +400,17 @@ let translate_v7_string dir = function
   | "simpl_plus_l" -> "plus_reg_l"
   | "simpl_plus_r" -> "plus_reg_r"
   | "fact_growing" -> "fact_le"
-  | "lt_mult_left" -> "lt_mult_S_left"
-  | "mult_le" -> "mult_le_l"
-  | "mult_le_right" -> "mult_le_r"
+  | "mult_assoc_l" -> "mult_assoc"
+  | "mult_assoc_r" -> "mult_assoc_reverse"
+  | "mult_1_n" -> "mult_1_l"
+  | "mult_n_1" -> "mult_1_r"
+  | "lt_mult_left" -> "mult_S_lt_compat_l"
+  | "mult_le" -> "mult_le_compat_l"
+  | "le_mult_right" -> "mult_le_compat_r"
+  | "le_mult_mult" -> "mult_le_compat"
+  | "mult_lt" -> "mult_S_lt_compat_l"
+  | "lt_mult_right" -> "mult_lt_compat_r"
+  | "mult_le_conv_1" -> "mult_S_le_reg_l"
   | "exists" -> "exists_between"
   | "IHexists" -> "IHexists_between"
   | "pred_Sn" -> "pred_S"