diff options
| author | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-03-28 07:15:20 -0700 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-03-28 16:15:20 +0200 |
| commit | 5e665ecc84eac83bd0a545995d161d83fbed9e25 (patch) | |
| tree | 75748780b3e6b288c0386b19cb5d71083d1bb7a5 /Makefile | |
| parent | fbc778079d50a4af45b9a648eab56cef29ac75f4 (diff) | |
| download | compcert-5e665ecc84eac83bd0a545995d161d83fbed9e25.tar.gz compcert-5e665ecc84eac83bd0a545995d161d83fbed9e25.zip | |
Change Implicit Arguments to Arguments (#225)
Implicit Arguments is deprecated in Coq since 8.6 or so.
Some Implicit Arguments remained in Flocq but were recently changed to Arguments.
Apply the same change to our local copy of Flocq.
As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 3 |
1 files changed, 0 insertions, 3 deletions
@@ -147,9 +147,6 @@ endif proof: $(FILES:.v=.vo) -# Turn off some warnings for compiling Flocq -flocq/%.vo: COQCOPTS+=-w -deprecated-implicit-arguments - extraction: extraction/STAMP extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMachdep.v |