From 5ec87d46f9392c6d569bbfe61060f0c548de0177 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 30 Oct 2003 14:26:00 +0000
Subject: traduction des noms de correctness

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4743 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/pmisc.ml    | 4 ++--
 contrib/correctness/psyntax.ml4 | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index ca7cee2e2e..ba96b98b71 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -110,7 +110,7 @@ let reset_names,pre_name,post_name,inv_name,
     (fun () -> next "for" forr Anonymous),
     (fun () -> string_of_id (next "Label" label Anonymous))
 
-let default = id_of_string "_"
+let default = id_of_string "x_"
 let id_of_name = function Name id -> id | Anonymous -> default
 
 
@@ -169,7 +169,7 @@ let coq_true = mkConstruct ((bool_sp,0),1)
 let coq_false = mkConstruct ((bool_sp,0),2)
 
 let constant s =
-  let id = id_of_string s in
+  let id = Constrextern.id_of_v7_string s in
   Termops.global_reference id
 
 let connective_and = id_of_string "prog_bool_and"
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index eab548215f..221445b58d 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -103,7 +103,7 @@ open Util
 open Coqast
 
 let mk_id loc id = mkRefC (Ident (loc, id))
-let mk_ref loc s = mk_id loc (id_of_string s)
+let mk_ref loc s = mk_id loc (Constrextern.id_of_v7_string s)
 let mk_appl loc1 loc2 f args =
   CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args)
 
-- 
cgit v1.2.3