diff options
author | 2018-02-24 23:55:09 -0800 | |
---|---|---|
committer | 2018-04-05 19:27:28 +0200 | |
commit | 4c392a12b726153d1a2d3e10280559285278aa6e (patch) | |
tree | d171c5cce8845898164e233394abab09c4047919 /vernac/vernacentries.ml | |
parent | 332efef9073eadb4907cd4e9ee1ba17bcc16afc6 (diff) |
Refactor impargs code.
This should preserve semantics exactly.
In the compute_implicits family of functions, I changed the
name of the pushed rel to not be fresh, but the env isn't passed
to find_displayed_name_in, and shouldn't affect whd_all.
Diffstat (limited to 'vernac/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions