diff options
| author | Maxime Dénès | 2016-06-30 15:18:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-01 17:26:02 +0200 |
| commit | 3e1e8e5792b43be83da2cca8102418aa9b73b9b3 (patch) | |
| tree | f46ebf80ac216adddf32bff2386114e0bf4d5ef0 /kernel/type_errors.ml | |
| parent | e57aab0559297cff3875931258674cfe2cfbbba3 (diff) | |
Make semantics of whd_zeta consistent with other whd_* functions.
whd_zeta now takes an evar_map and looks in evar instances. This changes
the behavior of whd_zeta e.g. on let x := ?t in x
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions