From 69c8917e3bdc8678baf1358ead549acff2f52ca2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 22 Aug 2018 15:53:09 +0200
Subject: Fix #8251: remove "the the" occurrences

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

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 7143f51853..d5d36c97fa 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -41,7 +41,7 @@ val register_alias : alias -> alias_tactic -> unit
 (** Register a tactic alias. *)
 
 val interp_alias : alias -> alias_tactic
-(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
+(** Recover the body of an alias. Raises an anomaly if it does not exist. *)
 
 val check_alias : alias -> bool
 (** Returns [true] if an alias is defined, false otherwise. *)
-- 
cgit v1.2.3