diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-01 18:09:57 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-01 18:32:53 +0200 |
commit | 5e310fc0456bc5123ab5aef255d61dde6ee8f4d7 (patch) | |
tree | 2a4600ac5f24ba9bd7a9f8e67828c70c9ece46b9 /META.coq | |
parent | 97ee8fbd0bf917c29e47f746c0a28623ebc7da9a (diff) |
Actually take advantage of the normalization status of kernel closures.
We know that when a fterm is marked as Whnf or Norm, the only thing that can
happen in the reduction machine is administrative reduction pushing the
destructured term on the stack. Thus there is no need to perform any
actual performative reduction.
Furthermore, every head subterm of those terms are recursively Whnf or Norm,
which implies that no update mark is pushed on the stack during the
destructuration. So there is no need to unzip the stack to unset FLOCKED
nodes as well.
Diffstat (limited to 'META.coq')
0 files changed, 0 insertions, 0 deletions