diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-26 20:21:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-04 21:13:26 +0200 |
| commit | 99c04392c7ad85811d61f72f89e6ec8207a2de2f (patch) | |
| tree | 55fbdcfa67d09b9fc0a696ffd645ca8cbfca24ca /pretyping/nativenorm.ml | |
| parent | d862b659457b12437d4fa348c3c4dc3dd08d8065 (diff) | |
Preserving "canonical" form of return predicate in vm_compute.
Note that the normalization of the context of the return predicate was
not done by the vm but by the lazy machine. The patch also "fixes" an
anomaly in the case of an arity which was not in canonical form as in:
Inductive A : nat -> id (nat->Type) := .
Eval vm_compute in fun x => match x in A y z return y = z with end.
Diffstat (limited to 'pretyping/nativenorm.ml')
0 files changed, 0 insertions, 0 deletions