| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
| |
Instead, add `Set Asymmetric Patterns` to the files that need it,
or use `Arguments` to make inductive types work better with symmetric patterns.
Closes: #403
|
| |
|
|
|
|
| |
The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.
|
| |
|
|
| |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The original presentation of forward_simulation and backward_simulation diagrams was using records containing types, relations, and properties over these. These records had to live in Type because in Prop the projections could not be defined.
This was causing problems with proofs of statements such as
(exists x, P x) -> forward_simulation sem1 sem2
because the exists could not be eliminated in a Type context.
This commit re-expresses the simulation diagrams as a record of properties (in Prop) and an inductive (in Prop too) that packs the record with the types and relations. The external interface of module Smallstep is unchanged, it's only the proofs in Smallstep and Behaviors that take a slightly different shape.
|
| | |
|
| |
|
|
|
|
|
| |
Update ARM port.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
of semantic preservation.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
