diff options
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index b73e7c7515..8a98a43ba0 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -504,8 +504,7 @@ let pr_intarg n = spc () ++ int n let pr_oc = function | None -> str" :" - | Some true -> str" :>" - | Some false -> str" :>>" + | Some () -> str" :>" let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) = let prx = match x with |