From 499d48cba16ce5f42eff82e99cf8e0e08c796f8b Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 11:10:23 +0200
Subject: typo

---
 tuto1/src/g_tuto1.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index da14d03842..78deabed94 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -1,7 +1,7 @@
 DECLARE PLUGIN "tuto1_plugin"
 
 (* If we forget this line and include our own tactic definition using
-  TACTIC EXTEND, as below, then we get the strage error message
+  TACTIC EXTEND, as below, then we get the strange error message
   no implementation available for Tacentries, only when compiling
   theories/Loader.v
 *)
-- 
cgit v1.2.3