diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d43b94ec4b..ddb85a3626 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -621,7 +621,10 @@ module Make | FullInversion -> primitive "inversion" | FullInversionClear -> primitive "inversion_clear" - let pr_lazy lz = if lz then keyword "lazy" else mt () + let pr_lazy = function + | General -> keyword "multi" + | Lazy -> keyword "lazy" + | Once -> mt () let pr_match_pattern pr_pat = function | Term a -> pr_pat a |