From 077bb33552ecaa08ea8974cd90a06a272f6ce2ab Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 27 Jun 2018 14:07:39 +0200
Subject: [PATCH] Temptative clarification of the role of ltac_genargs field in
 ltac_var_map.

---
 pretyping/ltac_pretype.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml
index be8579c2e580..ac59b96eefd4 100644
--- a/pretyping/ltac_pretype.ml
+++ b/pretyping/ltac_pretype.ml
@@ -64,5 +64,5 @@ type ltac_var_map = {
   ltac_idents: Id.t Id.Map.t;
   (** Ltac variables bound to identifiers *)
   ltac_genargs : unbound_ltac_var_map;
-  (** Ltac variables bound to other kinds of arguments *)
+  (** All Ltac variables (to pass on ltac subterms, and for error reporting) *)
 }