aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/spawn.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-06-30 15:18:21 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-01 17:26:02 +0200
commit3e1e8e5792b43be83da2cca8102418aa9b73b9b3 (patch)
treef46ebf80ac216adddf32bff2386114e0bf4d5ef0 /lib/spawn.ml
parente57aab0559297cff3875931258674cfe2cfbbba3 (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 'lib/spawn.ml')
0 files changed, 0 insertions, 0 deletions