From 2c67e51782ca27b4d6edbc0766650d8a2dad8f13 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 18 Mar 2022 15:06:41 -0400
Subject: [PATCH] fix a typo

---
 theories/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 2baea53c..79a5be44 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -27,7 +27,7 @@ Global Hint Extern 1001 => progress subst : subst. (** backtracking on this one
 be very bad, so use with care! *)
 
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
-is rather efficient when having big hint databases, or expensive [Hint Extern]
+is rather inefficient when having big hint databases, or expensive [Hint Extern]
 declarations as the ones above. *)
 Tactic Notation "intuition" := intuition auto.
 
-- 
GitLab