From 4687b08572b9032090b60402a2ede0e59bf97195 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 Sep 2003 18:42:03 +0000
Subject: Traduction de '_' comme reference

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

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d940aae37f..33e9ec72ce 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -126,6 +126,9 @@ let name_app f = function
   | Name id -> Name (f id)
   | Anonymous -> Anonymous
 
+let avoid_wildcard_string s =
+  if s = "_" then "x_" else s
+
 let avoid_wildcard id =
   if id = id_of_string "_" then id_of_string "x_" else id
 
@@ -220,11 +223,11 @@ let v7_to_v8_dir_id dir id =
     let s = string_of_id id in
     let s = 
       if (is_coq_root (Lib.library_dp()) or is_coq_root dir)
-      then translate_v7_string s else s in
+      then translate_v7_string s else avoid_wildcard_string s in
     id_of_string (translate_keyword s)
   else id
 
-let v7_to_v8_id id = avoid_wildcard (v7_to_v8_dir_id empty_dirpath id)
+let v7_to_v8_id id = v7_to_v8_dir_id empty_dirpath id
 
 let shortest_qualid_of_v7_global ctx ref =
   let fulldir,_ = repr_path (sp_of_global ref) in
-- 
cgit v1.2.3