From c881bc37b91a201f7555ee021ccb74adb360d131 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 15 Dec 2003 09:43:27 +0000
Subject: 'Eval' protege dans Ppconstrnew; eval n'a pas le meme besoin

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

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c3bcc16178..337c888a42 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -139,12 +139,15 @@ let rec translate_ident_string = function
       (str ("Warning: '"^
           s^"' is now a keyword; it has been translated to '"^s'^"'"));
       s'
+(* Le conflit est en fait surtout avec Eval dans Definition et c'est gere dans
+   Ppconstrnew
   | "eval" as s ->
       let s' = s^"_" in
       msgerrnl
       (str ("Warning: '"^
           s^"' is a conflicting ident; it has been translated to '"^s'^"'"));
       s'
+*)
 
   (* avoid _ *)
   | "_" -> 
-- 
cgit v1.2.3