Nouveaux renommages; mot-cle 'exists'

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

1 files changed, 44 insertions, 10 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b724becf13..01ed0cf98a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -137,7 +137,7 @@ let avoid_wildcard id =
 
 let translate_keyword = function
   | ("forall" | "fun" | "match" | "fix" | "cofix" | "for" | "let"
-    | "if"  | "then" | "else" | "return" | "mod" | "where" as s) ->
+    | "if"  | "then" | "else" | "return" | "mod" | "where" | "exists" as s) ->
       let s' = s^"_" in
       msgerrnl
       (str ("Warning: '"^
@@ -173,10 +173,12 @@ let translate_v7_string dir = function
   | "add_sym" -> "Pplus_comm"
   | "add_x_x" -> "Pplus_x_x"
   | "add_carry_add" -> "Pplus_carry_plus"
-  | "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"
+  | "simpl_add_r" -> "Pplus_reg_r"
+  | "simpl_add_l" -> "Pplus_reg_l"
+  | "simpl_add_carry_r" -> "Pplus_carry_reg_r"
+  | "simpl_add_carry_l" -> "Pplus_carry_reg_l"
+  | "simpl_times_r" -> "Pmult_reg_r"
+  | "simpl_times_l" -> "Pmult_reg_l"
 (*
   | "xO_xI_add_double_moins_un" -> "xO_xI_plus_double_minus_one"
 *)
@@ -247,8 +249,8 @@ let translate_v7_string dir = function
   | "Zmult_sym" -> "Zmult_comm"
   | "Zero_mult_left" -> "Zmult_0_l"
   | "Zero_mult_right" -> "Zmult_0_r"
-  | "Zmult_1_n" -> "Zmult_id_l"
-  | "Zmult_n_1" -> "Zmult_id_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"
@@ -305,7 +307,7 @@ let translate_v7_string dir = function
   | "Zeq_S" -> "Zs_eq_compat"
   | "Zs_pred" -> "Zs_pred"
   | "Zpred_Sn" -> "Zpred_Zs"
-  | "Zsimpl_plus_l" -> "Zplus_simpl_l"
+  | "Zsimpl_plus_l" -> "Zplus_reg_l"
   | "Zplus_simpl" -> "Zplus_eq_compat"
   | "POS_gt_ZERO" -> "Zpos_gt_0"
   | "ZERO_le_POS" -> "Z0_le_pos"
@@ -322,6 +324,23 @@ let translate_v7_string dir = function
   | "Zlt_not_sym" -> "Zlt_asym"
   | "Zlt_n_n" -> "Zlt_irrefl"
   | "Zgt_antirefl" -> "Zgt_irrefl"
+  | "Zgt_reg_l" -> "Zplus_gt_compat_l"
+  | "Zgt_reg_r" -> "Zplus_gt_compat_r"
+  | "Zlt_reg_l" -> "Zplus_lt_compat_l"
+  | "Zlt_reg_r" -> "Zplus_lt_compat_r"
+  | "Zle_reg_l" -> "Zplus_le_compat_l"
+  | "Zle_reg_r" -> "Zplus_le_compat_r"
+  | "Zlt_le_reg" -> "Zplus_lt_le_compat"
+  | "Zle_lt_reg" -> "Zplus_le_lt_compat"
+  | "Zle_mult_simpl" -> "Zmult_le_reg_r"
+  | "Zge_mult_simpl" -> "Zmult_ge_reg_r"
+  | "Zgt_mult_simpl" -> "Zmult_gt_reg_r"
+  | "Zsimpl_gt_plus_l" -> "Zplus_gt_reg_l"
+  | "Zsimpl_gt_plus_r" -> "Zplus_gt_reg_r"
+  | "Zsimpl_le_plus_l" -> "Zplus_le_reg_l"
+  | "Zsimpl_le_plus_r" -> "Zplus_le_reg_r"
+  | "Zsimpl_lt_plus_l" -> "Zplus_lt_reg_l"
+  | "Zsimpl_lt_plus_r" -> "Zplus_lt_reg_r"
   (* IntMap *)
   | "convert_xH" -> "IPN_xH"
   | "convert_xO" -> "IPN_xO"
@@ -342,13 +361,28 @@ let translate_v7_string dir = function
   | "lt_not_sym" -> "lt_asym"
   | "gt_antirefl" -> "gt_irrefl"
   | "lt_n_n" -> "lt_irrefl"
-  | "simpl_plus_l" -> "plus_simpl_l"
-  | "simpl_plus_r" -> "plus_simpl_r"
+  | "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"
   | "exists" -> "exists_between"
   | "IHexists" -> "IHexists_between"
   | "pred_Sn" -> "pred_S"
+  | "gt_reg_l" -> "plus_gt_compat_l"
+  | "le_reg_l" -> "plus_le_compat_l"
+  | "le_reg_r" -> "plus_le_compat_r"
+  | "lt_reg_l" -> "plus_lt_compat_l"
+  | "lt_reg_r" -> "plus_lt_compat_r"
+  | "le_plus_plus" -> "plus_le_compat"
+  | "le_lt_plus_plus" -> "plus_le_lt_compat"
+  | "lt_le_plus_plus" -> "plus_lt_le_compat"
+  | "lt_plus_plus" -> "plus_lt_compat"
+  | "plus_simpl_l" -> "plus_reg_l"
+  | "simpl_gt_plus_l" -> "plus_gt_reg_l"
+  | "simpl_le_plus_l" -> "plus_le_reg_l"
+  | "simpl_lt_plus_l" -> "plus_lt_reg_l"
   (* Init *)
   | "relation" when is_module "Datatypes" or is_dir dir "Datatypes"
       -> "comparison"