From f0a1b3b5ab118b5f5974ec7bf66bafae8121e0d3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Nov 2003 18:42:45 +0000
Subject: Conflit renommage

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

(limited to 'interp')

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"
 *)
-- 
cgit v1.2.3