diff options
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) *) } |