diff options
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 ########################################################################### |