diff --git a/Makefile b/Makefile index 4911acb..60c6f71 100644 --- a/Makefile +++ b/Makefile @@ -1,16 +1,18 @@ # -*- Makefile -*- -# -------------------------------------------------------------------- -DUNEOPTS ?= -DUNE := dune $(DUNEOPTS) +all: Makefile.coq + +make -f Makefile.coq all -# -------------------------------------------------------------------- -.PHONY: default build clean +clean: Makefile.coq + +make -f Makefile.coq clean + rm -f Makefile.coq Makefile.coq.conf -default: build +_CoqProject:; -build: - $(DUNE) build +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq -clean: - $(DUNE) clean +%: Makefile.coq + +make -f Makefile.coq $@ + +.PHONY: all clean diff --git a/_CoqProject b/_CoqProject index d8781a0..6d21035 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3,4 +3,11 @@ -arg -w -arg -redundant-canonical-projection -arg -w -arg -projection-no-head-constant --R _build/default/src SsrMultinomials +# -R _build/default/src SsrMultinomials +-R src SsrMultinomials + +src/ssrcomplements.v +src/monalg.v +src/xfinmap.v +src/mpoly.v +src/freeg.v diff --git a/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam index 4a7ee7b..fba71c4 100644 --- a/coq-mathcomp-multinomials.opam +++ b/coq-mathcomp-multinomials.opam @@ -6,7 +6,11 @@ bug-reports: "https://github.com/math-comp/multinomials/issues" dev-repo: "git+https://github.com/math-comp/multinomials.git" license: "CeCILL-B" authors: ["Pierre-Yves Strub"] -build: [ "dune" "build" "-p" name "-j" jobs ] +# build: [ "dune" "build" "-p" name "-j" jobs ] + +build: [make "-j%{jobs}%"] +install: [make "install"] + depends: [ "coq" {(>= "8.10" & < "8.14~") | = "dev"} "dune" {>= "2.5"}