| Age | Commit message (Collapse) | Author |
|---|
|
|
|
https://github.com/AbsInt/CompCert/issues/234
|
|
|
|
|
|
vm_compute and native_compute (partial fix to #7068; also fixes #7076))
|
|
|
|
|
|
Instead of having a constant-based compilation of projections, we
generate them at the compilation time of the inductive block to which
they pertain.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
When called by auto, `simple apply` still does not respect `Opaque`
because of compatibility issues.
|
|
Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
|
|
"rename" flag
|
|
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
git does not know how to fix this automatically when they appear by
removing a chunk of text at the end of the file.
eg
```
foo
bar
```
to
```
foo
```
|
|
|
|
kernel closures.
|
|
|
|
pattern-matching names
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We use an option type instead of returning a pair with a boolean. Indeed, the
boolean being true was always indicating that the returned value was unchanged.
The previous API was somewhat error-prone, and I don't understand why it was
designed this way in the first place.
|
|
tactic unification.
|
|
|
|
coinductive types.
|
|
|
|
|
|
|
|
of List
|
|
|
|
|
|
|
|
|
|
|
