diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-13 16:25:49 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-13 16:25:49 +0100 |
| commit | 8e7de2a327b202130192a784f921699f70e707cb (patch) | |
| tree | 1a9460251285bb124898a0c1c29c5531fc9017f6 /arm/Asm.v | |
| parent | e0aab135237aaa9334afe9acc9b519bbe2b53ae9 (diff) | |
| download | compcert-kvx-8e7de2a327b202130192a784f921699f70e707cb.tar.gz compcert-kvx-8e7de2a327b202130192a784f921699f70e707cb.zip | |
Turn warning "deprecated-implicit-arguments" off while compiling Flocq
Perhaps for reasons of backward compatibility with Coq 8.4, Flocq 2.5.2 still uses the "Implicit Arguments foo" idiom, which is deprecated in Coq 8.6.
Diffstat (limited to 'arm/Asm.v')
0 files changed, 0 insertions, 0 deletions