aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/ppvernac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 8e7af67b0c..b3a8abce55 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -820,7 +820,7 @@ let rec pr_vernac = function
(* For extension *)
| VernacExtend (s,c) -> pr_extend s c
- | VernacProof Tacexpr.TacId _ -> str "Proof"
+ | VernacProof (Tacexpr.TacId _) -> str "Proof"
| VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te
and pr_extend s cl =