From c1e7b28f5977eafd45c36c2ffdca9b7145d867bb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Oct 2020 18:57:10 +0200
Subject: Use same code for "Print Ltac foo" and "Print foo" when "foo" is an
 Ltac.

Adopting the same format means printing "Ltac foo := ..." and not the
fully qualified name of foo.
---
 plugins/ltac/tacintern.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'plugins/ltac/tacintern.mli')

diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 22ec15566b..f779aa470c 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -55,9 +55,6 @@ val intern_hyp : glob_sign -> lident -> lident
 
 val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
 
-(** printing *)
-val print_ltac : Libnames.qualid -> Pp.t
-
 (** Reduction expressions *)
 
 val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
-- 
cgit v1.2.3