aboutsummaryrefslogtreecommitdiff
path: root/coqpp/coqpp_main.ml
diff options
context:
space:
mode:
authorVincent Laporte2018-09-06 17:26:47 +0200
committerVincent Laporte2018-09-06 17:26:47 +0200
commit1877e1235c63ff3bbc958e5a79fa052ac852071c (patch)
treefb8c472cdf49424b9d6b4d83da84299ce2f6e2bb /coqpp/coqpp_main.ml
parentaf30a9a70221d8dee3b837664d372becbbf71762 (diff)
deprecation is CODE instead of IDENT
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