diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-26 20:22:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-04 21:13:26 +0200 |
| commit | ef052549cddf35eed9603caf3c451cec41013078 (patch) | |
| tree | f66f5a1f00c78905d917ea19c2339e932889c131 /test-suite/bugs | |
| parent | 99c04392c7ad85811d61f72f89e6ec8207a2de2f (diff) | |
Preserving "canonical" form of return predicate in native_compute.
Note that the normalization of the context of the return predicate was
not done by the native compilation 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 native_compute in fun x => match x in A y z return y = z with end.
Diffstat (limited to 'test-suite/bugs')
0 files changed, 0 insertions, 0 deletions