diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b7b8e1bb27..63a48ee70a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -316,8 +316,8 @@ let translate_v7_string dir = function | "compare_convert_O" -> "lt_O_nat_of_P" | "Zopp_intro" -> "Zopp_inj" | "plus_iter_add" -> "plus_iter_eq_plus" - | "add_verif" -> "Pmult_nat_plus_morphism" - | "ZL2" -> "Pmult_nat_plus_morphism" + | "add_verif" -> "Pmult_nat_l_plus_morphism" + | "ZL2" -> "Pmult_nat_r_plus_morphism" (* Trop spécifique ? | "ZL6" -> "Pmult_nat_plus_shift_morphism" *) |