diff options
| author | herbelin | 2003-11-26 21:27:48 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-26 21:27:48 +0000 |
| commit | 993b785abefb2c1bcc0428836a601e73bae6a344 (patch) | |
| tree | a2f9d13b59559070b00f535cd4c3a05ea8f10b04 /contrib/correctness/psyntax.ml4 | |
| parent | 08a34ea65168c36720eb555df02aa69b84e29466 (diff) | |
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
Diffstat (limited to 'contrib/correctness/psyntax.ml4')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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) |