aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppvernac.ml')
-rw-r--r--parsing/ppvernac.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c50b2e52f..b181247ab 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -572,6 +572,9 @@ let rec pr_vernac = function
| CWfRec c ->
spc() ++ str "{wf " ++ pr_name name ++ spc() ++
pr_lconstr_expr c ++ str"}"
+ | CMeasureRec c ->
+ spc() ++ str "{measure " ++ pr_name name ++ spc() ++
+ pr_lconstr_expr c ++ str"}"
in
pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_