From e6322e23958a937fa01960f8ce320717b9863253 Mon Sep 17 00:00:00 2001
From: JPR
Date: Tue, 21 May 2019 23:07:55 +0200
Subject: Fixing typos - Part 1

---
 dev/doc/proof-engine.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/doc/proof-engine.md')

diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
index 774552237a..a2c8d2f5ac 100644
--- a/dev/doc/proof-engine.md
+++ b/dev/doc/proof-engine.md
@@ -121,7 +121,7 @@ a limited set of derivation rules), it is recommended to generate proofs as
 much as possible by refining in ML tactics when it is possible and easy enough.
 Indeed, this prevents dependence on fragile constructions such as unification.
 
-Obviously, it does not forbid the use of tacticals to mimick what one would do
+Obviously, it does not forbid the use of tacticals to mimic what one would do
 in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple
 semantics. A list of such tacticals can be found in the `Tacticals` module. Most
 of them are a porting of the tacticals from the old engine to the new one, so
-- 
cgit v1.2.3