aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppvernac.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a5235a25fa..b6ab7a2382 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -861,6 +861,7 @@ let rec pr_vernac = function
| `ReductionNeverUnfold -> str "simpl never"
| `DefaultImplicits -> str "default implicits"
| `Rename -> str "rename"
+ | `Assert -> str "assert"
| `ExtraScopes -> str "extra scopes"
| `ClearImplicits -> str "clear implicits"
| `ClearScopes -> str "clear scopes")