From 394c8d20036bd502d8ba03d61080017b4bff86c8 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 18 Jul 2021 14:32:36 +0000
Subject: [PATCH] fix typo

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

diff --git a/theories/tactics.v b/theories/tactics.v
index ba96fded..6ed5877f 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -227,7 +227,7 @@ Note that the obvious alternative [open_constr (_:T)] has subtly different
 behavior, see std++ issue 115.
 
 Usually, Ltacs cannot return a value and have a side-effect, but we use the
-trickd escribed at
+trick described at
 <https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884>
 to work around that: wrap the side-effect in a [match goal]. *)
 Ltac mk_evar T :=
-- 
GitLab