From 64b9e9fd6290024431fbcfdbb8aaad4d4b9cc1f9 Mon Sep 17 00:00:00 2001
From: Enrico
Date: Thu, 17 May 2018 17:08:09 +0200
Subject: [tuto1] Minor fixes to comments

---
 tuto1/src/g_tuto1.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index 78deabed94..bd53053ec7 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -7,7 +7,8 @@ DECLARE PLUGIN "tuto1_plugin"
 *)
 open Ltac_plugin
 open Pp
-(* This one is necessary, to avoid message about missing wit_string *)
+(* This module defines the types of arguments to be used in the
+   EXTEND directives below, for example the string one. *)
 open Stdarg
 
 VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
@@ -68,7 +69,7 @@ END
 (* When adding a definition, we have to be careful that just
   the operation of constructing a well-typed term may already change
   the environment, at the level of universe constraints (which
-  are recorded in the evd component).  The fonction
+  are recorded in the evd component).  The function
   Constrintern.interp_constr ignores this side-effect, so it should
   not be used here. *)
 
-- 
cgit v1.2.3