summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-30 21:35:44 +0200
committerNadrieril2019-04-30 21:35:44 +0200
commit1c7435009d364e493fbc0f58c1187691ce973992 (patch)
tree716a1603e635b162c4171c7602aa82ae063e106b
parent8a846a6b0af141b45e7f92da7ecad32c89d581f8 (diff)
Fix NF tracking error
-rw-r--r--dhall/src/normalize.rs5
1 files changed, 3 insertions, 2 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 85cadca..dbb6d95 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -1060,8 +1060,9 @@ mod thunk {
e.clone(),
)
}
- ThunkInternal::Value(m, v) => {
- ThunkInternal::Value(*m, v.subst_shift(var, val))
+ ThunkInternal::Value(_, v) => {
+ // The resulting value may not stay in normal form after substitution
+ ThunkInternal::Value(WHNF, v.subst_shift(var, val))
}
}
}