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/globEnv.ml | |
| parent | 09482343fec8cd40b1f9523be8e5e2601eb0bbae (diff) | |
Temptative clarification of the role of ltac_genargs field in ltac_var_map.
Diffstat (limited to 'pretyping/globEnv.ml')
0 files changed, 0 insertions, 0 deletions