diff options
| author | Hugo Herbelin | 2018-06-27 14:07:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:27:50 +0200 |
| commit | 077bb33552ecaa08ea8974cd90a06a272f6ce2ab (patch) | |
| tree | 7e4b85f29323c0e270b8c947fb28662aeaf48b15 /pretyping | |
| parent | 09482343fec8cd40b1f9523be8e5e2601eb0bbae (diff) | |
Temptative clarification of the role of ltac_genargs field in ltac_var_map.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/ltac_pretype.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml index be8579c2e5..ac59b96eef 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) *) } |