diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-09 21:08:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-09 21:08:46 +0000 |
| commit | b797be200ab9e334222dac622e8ec07f240292b4 (patch) | |
| tree | 69c87ecf675158c3dcf492d030ee995e55c9d348 /interp/constrextern.ml | |
| parent | 976682eec9903bd24ed2d23c2b97f43b5996a861 (diff) | |
Quelqes renommages lies a Zorder
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4846 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 338457668..9d6dd3c4f 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" |