Nouvelle serie de traductions

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

1 files changed, 39 insertions, 9 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2eae4a51b..54b782f0c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -165,21 +165,40 @@ let translate_v7_string = function
   | "add_assoc" -> "Pplus_assoc"
   | "add_sym" -> "Pplus_comm"
   | "add_x_x" -> "Pplus_x_x"
+  | "add_carry_add" -> "Pplus_carry_Pplus"
   | "simpl_add_r" -> "Pplus_simpl_r"
   | "simpl_add_l" -> "Pplus_simpl_l"
+  | "simpl_add_carry_r" -> "Pplus_carry_simpl_r"
+  | "simpl_add_carry_l" -> "Pplus_carry_simpl_l"
+  | "xO_xI_add_double_moins_un" -> "xO_xI_Pplus_Pdouble_minus_one"
+  | "double_moins_un_plus_xO_double_moins_un" ->
+      "Pdouble_minus_one_Pplus_xO_Pdouble_minus_one"
+  | "add_xI_double_moins_un" -> "add_xI_double_minus_one"
   | "iter_pos_add" -> "iter_pos_Pplus"
+  | "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_Pplus_distr"
-  | "times_true_sub_distr" -> "Pmult_Pminus_distr"
+  | "times_add_distr" -> "Pmult_Pplus_distr_r"
+  | "times_add_distr_l" -> "Pmult_Pplus_distr_l"
+  | "times_true_sub_distr" -> "Pmult_Pminus_distr_r"
   | "times_sym" -> "Pmult_comm"
   | "times_assoc" -> "Pmult_assoc"
   | "times_convert" -> "IPN_Pmult_morphism"
   | "true_sub" -> "Pminus"
+  | "times_x_1" -> "Pmult_1_right"
+  | "times_x_double" -> "Pmult_xO_permute_r"
+  | "times_x_double_plus_one" -> "Pmult_xI_permute_r"
   | "true_sub_convert" -> "IPN_Pminus_morphism"
+  | "compare_true_sub_right" -> "Pcompare_Pminus_r"
+  | "compare_true_sub_left" -> "Pcompare_Pminus_l"
   | "sub_add" -> "Lt_Pplus_Pminus" (* equiv de le_plus_minus de Arith *)
   | "sub_add_one" -> "Ppred_Psucc"
   | "add_sub_one" -> "Psucc_Ppred"
   | "add_un" -> "Psucc"
+  | "add_un_inj" -> "Psucc_inj"
+  | "xI_add_un_xO" -> "xI_Psucc_xO"
+  | "ZL14" -> "Pplus_Psucc_permute_r"
+  | "ZL14bis" -> "Pplus_Psucc_permute_l"
   | "sub_un" -> "Ppred"
   | "sub_pos" -> "PNminus"
   | "sub_pos_x_x" -> "PNminus_x_x"
@@ -188,7 +207,13 @@ let translate_v7_string = function
   | "Nul" -> "Null"
   | "Un_suivi_de" -> "double_plus_one"
   | "Zero_suivi_de" -> "double"
-  | "is_double_moins_un" -> "is_Pdouble_minus_one"
+  | "ZS" -> "double_eq_zero_inversion"
+  | "US" -> "double_plus_one_zero_discr"
+  | "USH" -> "double_plus_one_eq_one_inversion"
+  | "ZSH" -> "double_eq_one_discr"
+  | "is_double_moins_un" -> "Psucc_Pdouble_minus_one_xO"
+  | "double_moins_un_add_un_xI" -> "Pdouble_minus_one_Psucc_xI"
+  | "ZL1" -> "xO_Psucc_permute"
   | "Zplus_sym" -> "Zplus_comm"
   | "Zmult_sym" -> "Zmult_comm"
   | "inject_nat" -> "INZ"
@@ -208,18 +233,23 @@ let translate_v7_string = function
   | "add_verif" -> "IPN_shift_Pplus_morphism"
   | "cvt_carry" -> "IPN_Pplus_carry"
   | "iter_convert" -> "iter_IPN"
-  | "compare_convert1" -> "compare_not_Eq"
-  | "compare_convert_INFERIEUR" -> "IPN_lt_morphism_compare"
-  | "compare_convert_SUPERIEUR" -> "IPN_gt_morphism_compare"
+  | "compare" -> "Pcompare"
+  | "compare_convert1" -> "Pcompare_not_Eq"
+  | "compare_convert_INFERIEUR" -> "IPN_lt_morphism1_Pcompare"
+  | "compare_convert_SUPERIEUR" -> "IPN_gt_morphism1_Pcompare"
   | "compare_convert_EGAL"      -> "compare_Eq_eq"
-  | "convert_compare_INFERIEUR" -> "IPN_lt_surj_morphism_compare"
-  | "convert_compare_SUPERIEUR" -> "IPN_gt_surj_morphism_compare"
-  | "convert_compare_EGAL"      -> "compare_refl"
+  | "convert_compare_INFERIEUR" -> "IPN_lt_morphism2_Pcompare"
+  | "convert_compare_SUPERIEUR" -> "IPN_gt_morphism2_Pcompare"
+  | "convert_compare_EGAL"      -> "Pcompare_refl"
   | "Zcompare_EGAL"             -> "Zcompare_Eq_eq"
   | "Zcompare_et_un"            -> "Zcompare_Gt_not_Lt"
   | "Zcompare_trans_SUPERIEUR"  -> "Zcompare_Gt_trans"
   | "SUPERIEUR_POS"             -> "Zcompare_Gt_POS"
   | "compare_positive_to_nat_O" -> "le_IPN_shift"
+  | "ZLSI" -> "ZLGtLt"
+  | "ZLIS" -> "ZLLtGt"
+  | "ZLII" -> "ZLLtLt"
+  | "ZLSS" -> "ZLGtGt"
   | "bij1" -> "IPN_INP_succ_eq_succ"
   | "bij2" -> "INP_succ_IPN_eq_succ"
   | "bij3" -> "pred_INP_succ_IPN_bij"