Remplacement de l'indicateur de date "@" par 'at'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4998 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 8 insertions, 5 deletions

diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 5fbcf4489f..ce1f69dccc 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -49,20 +49,23 @@ let reraise_with_loc loc f x =
 
 (* functions on names *)
 
-let at_id id d = id_of_string ((string_of_id id) ^ "@" ^ d)
+let at = if !Options.v7 then "@" else "'at'"
+
+let at_id id d = id_of_string ((string_of_id id) ^ at ^ d)
 
 let is_at id =
   try
-    let _ = String.index (string_of_id id) '@' in true
+    let _ = string_index_from (string_of_id id) 0 at in true
   with Not_found ->
     false
 
 let un_at id =
   let s = string_of_id id in
     try
-      let n = String.index s '@' in
+      let n = string_index_from s 0 at in
     	id_of_string (String.sub s 0 n),
-	String.sub s (succ n) (pred (String.length s - n))
+	String.sub s (n + String.length at)
+          (String.length s - n - String.length at)
     with Not_found ->
       invalid_arg "un_at"
 
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 47ee5d84b5..402537e509 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -1025,7 +1025,7 @@ let rec pr_desc = function
       (* Numeral or "tt": use a printer which doesn't globalize *)
       Ppconstr.pr_constr
         (Constrextern.extern_constr_in_scope false "Z_scope" (Global.env()) c)
-  | Debug (s,p) -> str "@" ++ pr_prog p
+  | Debug (s,p) -> str "@" ++ Pptacticnew.qsnew s ++ pr_prog p
 
 and pr_block_st = function
   | Label s -> hov 0 (str "label" ++ spc() ++ str s)