| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
|
|
|
|
| |
These minor problems were revealed by porting CompCert to Coq 8.6, where
they trigger errors.
|
|
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
| |
|
|
(Merge of branch newparser.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|