| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
| |
BigNumPrelude will soon leave Coq stdlib with the rest of the bignum
library (apart from Int31 files) to become a separate package.
With this (very minor) patch, Compcert compiles with or without
the hints declared in BigNumPrelude.
|
|
|
|
|
| |
This silences a warning of Coq 8.6.
Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
|
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2521 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
(Merge of branch newparser.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|