From ede77b72328c98995c0636656bb71ba87861ddfe Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 11 Oct 2020 19:15:51 -0700
Subject: Rename tactic_expr -> ltac_expr

---
 plugins/ltac/pptactic.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 6a9fb5c2ea..5e199dad62 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** This module implements pretty-printers for tactic_expr syntactic
+(** This module implements pretty-printers for ltac_expr syntactic
     objects and their subcomponents. *)
 
 open Genarg
-- 
cgit v1.2.3