diff options
| -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" |