diff options
| author | herbelin | 2003-11-14 18:42:45 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-14 18:42:45 +0000 |
| commit | f0a1b3b5ab118b5f5974ec7bf66bafae8121e0d3 (patch) | |
| tree | d370783d3b8509e4ce96f14606a07bf79cb11c02 | |
| parent | abaea95f6dd9c41d62b98e53bd0d36e4a1c75153 (diff) | |
Conflit renommage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4913 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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" *) |