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 3553373fb..686d2ae2d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -175,10 +175,6 @@ let pr_set_option a b = let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)" -let pr_destruct_location = function - | Tacexpr.ConclLocation () -> str"Conclusion" - | Tacexpr.HypLocation b -> if b then str"Discardable Hypothesis" else str"Hypothesis" - let pr_opt_hintbases l = match l with | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z |