diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f0c8cd58c..3e41439c8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -394,10 +394,6 @@ open Decl_kinds (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ str":" ++ pr_spc_lconstr c) - let pr_priority = function - | None -> mt () - | Some i -> spc () ++ str "|" ++ spc () ++ int i - (**************************************) (* Pretty printer for vernac commands *) (**************************************) |