From 9cc12b684ee6833971c9549aa76cc683ba931090 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 21 Apr 2020 22:08:07 +0200
Subject: begin scripting the Compiler.v file

---
 Makefile | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index a69f7e2e..2f9ab029 100644
--- a/Makefile
+++ b/Makefile
@@ -201,6 +201,8 @@ tools/ndfun: tools/ndfun.ml
 	ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml
 tools/modorder: tools/modorder.ml
 	ocamlopt -o tools/modorder str.cmxa tools/modorder.ml
+tools/compiler_expand: tools/compiler_expand.ml
+	ocamlopt -o $@ $+
 
 latexdoc:
 	cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)
@@ -216,6 +218,9 @@ latexdoc:
 	@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
 	@chmod a-w $*.v
 
+driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand
+	tools/compiler_expand driver/Compiler.vexpand $@
+
 compcert.ini: Makefile.config
 	(echo "stdlib_path=$(LIBDIR)"; \
          echo "prepro=$(CPREPRO)"; \
-- 
cgit