diff options
| -rw-r--r-- | contrib/correctness/pmisc.ml | 11 | ||||
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 2 |
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) |