diff options
| author | Matthieu Sozeau | 2014-06-26 11:05:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-26 11:05:00 +0200 |
| commit | 83ae5e6ad95372912ba9eb9f8c52d857cdf10021 (patch) | |
| tree | 6698ac68f45940456cafb56aaaf0dec36bfb408f /kernel/type_errors.mli | |
| parent | f6382ef326099651cd051aa907b4e9ac6c905698 (diff) | |
Change interface of refresh universes to get a pbty argument instead of
the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions