From 767816eece27e6bb8cba0bbf122507bd2a3b77a1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Nov 2017 22:54:24 +0100 Subject: Using a specific function to register vernac printers. --- plugins/ltac/g_obligations.ml4 | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'plugins/ltac/g_obligations.ml4') diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1a2d89586..fea9e837b 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -155,6 +155,4 @@ let () = | None -> mt () | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy + Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer -- cgit v1.2.3