diff options
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index af1f66c739..e5d7d75bd9 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -492,6 +492,7 @@ let rec pr_vernac = function | ShowTree -> str"Show Tree" | ShowProofNames -> str"Show Conjectures" | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro") + | ShowMatch id -> str"Show Match " ++ pr_lident id | ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l in pr_showable s |