Commit 58842ac2 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

[Dk] Enable most linearity checks

The only remaining non-linear file is non-linear on purpose
parent e5062e21
...@@ -50,7 +50,7 @@ SKCHECK=skcheck ...@@ -50,7 +50,7 @@ SKCHECK=skcheck
SKDEP=skdep SKDEP=skdep
DKDEP=dkdep DKDEP=dkdep
CONFLUENCECHECKER=$(shell locate csiho.sh) CONFLUENCECHECKER=$(shell locate csiho.sh)
DKCHECKOPTIONS=-nl -errors-in-snf -v -d # -cc $(CONFLUENCECHECKER) DKCHECKOPTIONS=-v -d #-cc $(CONFLUENCECHECKER)
DKDEPOPTIONS=-v DKDEPOPTIONS=-v
all: $(DKOS) sigmaid all: $(DKOS) sigmaid
...@@ -60,6 +60,8 @@ builtins.dko: builtins.dk ...@@ -60,6 +60,8 @@ builtins.dko: builtins.dk
%.dko: %.sk %.dko: %.sk
$(SKCHECK) -e $(DKCHECKOPTIONS) $< $(SKCHECK) -e $(DKCHECKOPTIONS) $<
dk_obj_dec.dko: dk_obj_dec.sk
$(SKCHECK) -e -nl $<
.v.vo: .v.vo:
coqc $< coqc $<
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment