From b797be200ab9e334222dac622e8ec07f240292b4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Nov 2003 21:08:46 +0000
Subject: Quelqes renommages lies a Zorder

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4846 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 338457668f..9d6dd3c4f5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -308,6 +308,7 @@ let translate_v7_string dir = function
   | "bij1" -> "IPN_INP_succ_eq_succ"
   | "bij2" -> "INP_succ_IPN_eq_succ"
   | "bij3" -> "pred_INP_succ_IPN_bij"
+  | "POS_inject" -> "Zpos_eq_INZ_IPN"
   | "absolu" -> "Zabs_nat"
   | "absolu_lt" -> "Zabs_nat_lt" (* "Zabs_nat_lt_morphism_pos" ? *)
   | "Zeq_add_S" -> "Zs_inj"
@@ -357,9 +358,9 @@ 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_right2" -> "Zmult_lt_reg_r"
+  | "Zlt_Zmult_right2" -> "Zmult_gt_0_lt_reg_r"
   | "Zlt_Zmult_right" -> "Zmult_gt_0_lt_compat_r"
-  | "Zle_Zmult_right2" -> "Zmult_le_reg_r"
+  | "Zle_Zmult_right2" -> "Zmult_gt_0_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"
-- 
cgit v1.2.3