ajout Pnat et Pcompare_antisym

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

1 files changed, 39 insertions, 36 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 90034e4971..6c7a6f5b1b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -157,6 +157,7 @@ let is_module m = is_dir (Lib.library_dp()) m
 let bp = ["BinPos"]
 let bz = ["BinInt"]
 let bn = ["BinNat"]
+let pn = ["nat"]
 let zc = ["Zcompare"]
 let lo = ["Logic"]
 let da = ["Datatypes"]
@@ -329,30 +330,40 @@ let translate_v7_string dir = function
   | "convert" -> bp,"nat_of_P"
   | "anti_convert" -> bp,"P_of_succ_nat"
   | "positive_to_nat" -> bp,"Pmult_nat"
-  | "convert_intro" -> bp,"nat_of_P_inj"
-  | "convert_add" -> bp,"nat_of_P_plus_morphism"
-  | "convert_add_un" -> bp,"Pmult_nat_succ_morphism"
-  | "cvt_add_un" -> bp,"nat_of_P_succ_morphism"
-  | "convert_add_carry" -> bp,"Pmult_nat_plus_carry_morphism"
-  | "compare_convert_O" -> bp,"lt_O_nat_of_P"
   | "Zopp_intro" -> bz,"Zopp_inj"
   | "plus_iter_add" -> bp,"plus_iter_eq_plus"
-  | "add_verif" -> bp,"Pmult_nat_l_plus_morphism"
-  | "ZL2" -> bp,"Pmult_nat_r_plus_morphism"
+  | "compare" -> bp,"Pcompare"
+  | "iter_convert" -> ["Zmisc"],"iter_nat_of_P"
+  | "ZLSI" -> bp,"Pcompare_Gt_Lt"
+  | "ZLIS" -> bp,"Pcompare_Lt_Gt"
+  | "ZLII" -> bp,"Pcompare_Lt_Lt"
+  | "ZLSS" -> bp,"Pcompare_Gt_Gt"
+  (* Pnat *)
+  | "convert_intro" -> pn,"nat_of_P_inj"
+  | "convert_add" -> pn,"nat_of_P_plus_morphism"
+  | "convert_add_un" -> pn,"Pmult_nat_succ_morphism"
+  | "cvt_add_un" -> pn,"nat_of_P_succ_morphism"
+  | "convert_add_carry" -> pn,"Pmult_nat_plus_carry_morphism"
+  | "compare_convert_O" -> pn,"lt_O_nat_of_P"
+  | "add_verif" -> pn,"Pmult_nat_l_plus_morphism"
+  | "ZL2" -> pn,"Pmult_nat_r_plus_morphism"
+  | "compare_positive_to_nat_O" -> pn,"le_Pmult_nat"
 (* Trop spécifique ?
-  | "ZL6" -> bp,"Pmult_nat_plus_shift_morphism"
+  | "ZL6" -> pn,"Pmult_nat_plus_shift_morphism"
 *)
-  | "ZL15" -> bp,"Pplus_carry_pred_eq_plus"
-  | "cvt_carry" -> bp,"nat_of_P_plus_carry_morphism"
-  | "iter_convert" -> ["Zmisc"],"iter_nat_of_P"
-  | "compare" -> bp,"Pcompare"
-  | "compare_convert1" -> bp,"Pcompare_not_Eq"
-  | "compare_convert_INFERIEUR" -> bp,"nat_of_P_lt_Lt_compare_morphism"
-  | "compare_convert_SUPERIEUR" -> bp,"nat_of_P_gt_Gt_compare_morphism"
-  | "compare_convert_EGAL"      -> bp,"Pcompare_Eq_eq"
-  | "convert_compare_INFERIEUR" -> bp,"nat_of_P_lt_Lt_compare_complement_morphism"
-  | "convert_compare_SUPERIEUR" -> bp,"nat_of_P_gt_Gt_compare_complement_morphism"
-  | "convert_compare_EGAL"      -> bp,"Pcompare_refl"
+  | "ZL15" -> pn,"Pplus_carry_pred_eq_plus"
+  | "cvt_carry" -> pn,"nat_of_P_plus_carry_morphism"
+  | "compare_convert1" -> pn,"Pcompare_not_Eq"
+  | "compare_convert_INFERIEUR" -> pn,"nat_of_P_lt_Lt_compare_morphism"
+  | "compare_convert_SUPERIEUR" -> pn,"nat_of_P_gt_Gt_compare_morphism"
+  | "compare_convert_EGAL"      -> pn,"Pcompare_Eq_eq"
+  | "convert_compare_INFERIEUR" -> pn,"nat_of_P_lt_Lt_compare_complement_morphism"
+  | "convert_compare_SUPERIEUR" -> pn,"nat_of_P_gt_Gt_compare_complement_morphism"
+  | "convert_compare_EGAL"      -> pn,"Pcompare_refl"
+  | "bij1" -> pn,"nat_of_P_o_P_of_succ_nat_eq_succ"
+  | "bij2" -> pn,"P_of_succ_nat_o_nat_of_P_eq_succ"
+  | "bij3" -> pn,"pred_o_P_of_succ_nat_o_nat_of_P_eq_id"
+  (* Zcompare *)
   | "Zcompare_EGAL"             -> zc,"Zcompare_Eq_iff_eq"
   | "Zcompare_EGAL_eq"          -> zc,"Zcompare_Eq_eq"
   | "Zcompare_x_x"              -> zc,"Zcompare_refl"
@@ -360,17 +371,9 @@ let translate_v7_string dir = function
   | "Zcompare_trans_SUPERIEUR"  -> zc,"Zcompare_Gt_trans"
   | "Zcompare_n_S"              -> zc,"Zcompare_succ_compat"
   | "SUPERIEUR_POS"             -> zc,"Zcompare_Gt_spec"
-  | "Zcompare_ANTISYM"          -> zc,"Zcompare_antisym"
-  | "compare_positive_to_nat_O" -> bp,"le_Pmult_nat"
+  | "Zcompare_ANTISYM"          -> zc,"Zcompare_Gt_Lt_antisym"
   | "Zcompare_Zs_SUPERIEUR"     -> zc,"Zcompare_succ_Gt"
   | "Zcompare_Zopp"             -> zc,"Zcompare_opp"
-  | "ZLSI" -> bp,"Pcompare_Gt_Lt"
-  | "ZLIS" -> bp,"Pcompare_Lt_Gt"
-  | "ZLII" -> bp,"Pcompare_Lt_Lt"
-  | "ZLSS" -> bp,"Pcompare_Gt_Gt"
-  | "bij1" -> bp,"nat_of_P_o_P_of_succ_nat_eq_succ"
-  | "bij2" -> bp,"P_of_succ_nat_o_nat_of_P_eq_succ"
-  | "bij3" -> bp,"pred_o_P_of_succ_nat_o_nat_of_P_eq_id"
   | "POS_inject" -> zn,"Zpos_eq_Z_of_nat_o_nat_of_P"
   | "absolu" -> bz,"Zabs_nat"
   | "absolu_lt" -> zabs,"Zabs_nat_lt" (* "Zabs_nat_lt_morphism_pos" ? *)
@@ -448,13 +451,13 @@ let translate_v7_string dir = function
   | "Zle_Zcompare" -> zo,"Zle_compare"
   | "Zgt_Zcompare" -> zo,"Zgt_compare"
   | "Zge_Zcompare" -> zo,"Zge_compare"
-  (* IntMap *)
-  | "convert_xH" -> bp,"nat_of_P_xH"
-  | "convert_xO" -> bp,"nat_of_P_xO"
-  | "convert_xI" -> bp,"nat_of_P_xI"
-  | "positive_to_nat_mult" -> bp,"Pmult_nat_mult_permute"
-  | "positive_to_nat_2" -> bp,"Pmult_nat_2_mult_2_permute"
-  | "positive_to_nat_4" -> bp,"Pmult_nat_4_mult_2_permute"
+  (* ex-IntMap *)
+  | "convert_xH" -> pn,"nat_of_P_xH"
+  | "convert_xO" -> pn,"nat_of_P_xO"
+  | "convert_xI" -> pn,"nat_of_P_xI"
+  | "positive_to_nat_mult" -> pn,"Pmult_nat_mult_permute"
+  | "positive_to_nat_2" -> pn,"Pmult_nat_2_mult_2_permute"
+  | "positive_to_nat_4" -> pn,"Pmult_nat_4_mult_2_permute"
   (* ZArith and Arith orders *)
   | "Zle_refl" -> zo,"Zeq_le"
   | "Zle_n" -> zo,"Zle_refl"