diff options
| author | Jason Gross | 2019-03-31 14:33:55 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-04-01 11:08:54 -0400 |
| commit | b0f8e09c3212fa96934817e7ca99465cd634f57c (patch) | |
| tree | 645e8114a3e86de4fd9d833523d87e6d20ceebb5 /kernel/nativelambda.mli | |
| parent | 606aa700cc258ceb01abbead42d38ef2e31ad6cd (diff) | |
[interp] [numeral] Use cbv rather than vm
It is important to fully normalize the term, *including inductive
parameters of constructors*; see https://github.com/coq/coq/issues/9840
for details on what goes wrong if this does not happen, e.g., from using
the vm rather than cbv.
Supersedes / closes #9655
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions