diff options
| author | letouzey | 2008-05-08 14:50:59 +0000 |
|---|---|---|
| committer | letouzey | 2008-05-08 14:50:59 +0000 |
| commit | e5a5332c96da9d65359c7a729a9c3fc81fb026d9 (patch) | |
| tree | ee0ad18d348c55e660b7c1a64212a9b4e45f7b26 /Makefile.build | |
| parent | 47a3b5afc264a45076a519682c094e207d4d210e (diff) | |
Integration of theories/Ints into theories/Numbers, part 3: auto-generation of NMake.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10902 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build index 35786edf8a..5536ea7754 100644 --- a/Makefile.build +++ b/Makefile.build @@ -523,6 +523,12 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQTOP) -dump-glob theories/Init/$*.glob -nois -compile theories/Init/$* +theories/Numbers/Natural/BigN/genN: theories/Numbers/Natural/BigN/genN.ml + $(OCAMLC) -o $@ $< + +theories/Numbers/Natural/BigN/NMake.v: theories/Numbers/Natural/BigN/genN + $< > $@ + ########################################################################### # tools ########################################################################### |