aboutsummaryrefslogtreecommitdiff
path: root/coqpp/coqpp_main.ml
diff options
context:
space:
mode:
Diffstat (limited to 'coqpp/coqpp_main.ml')
-rw-r--r--coqpp/coqpp_main.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index c1b94b5ebb..a8ed95f5ba 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -319,7 +319,7 @@ let print_ast fmt ext =
let deprecation fmt =
function
| None -> ()
- | Some s -> fprintf fmt "~deprecation:%s " s
+ | Some { code } -> fprintf fmt "~deprecation:(%s) " code
in
let pr fmt () =
let level = match ext.tacext_level with None -> 0 | Some i -> i in