diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-02-24 23:55:09 -0800 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-05 19:27:28 +0200 |
| commit | 4c392a12b726153d1a2d3e10280559285278aa6e (patch) | |
| tree | d171c5cce8845898164e233394abab09c4047919 /library/declaremods.mli | |
| 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 'library/declaremods.mli')
0 files changed, 0 insertions, 0 deletions