aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 8 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 3ed55298ec..dd7c67c889 100644
--- a/Makefile
+++ b/Makefile
@@ -1511,6 +1511,14 @@ proofs/tacexpr.cmx: proofs/tacexpr.ml
$(SHOW)'OCAMLOPT -rectypes $<'
$(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $<
+translate/pptacticnew.cmo: translate/pptacticnew.ml
+ $(SHOW)'OCAMLC -rectypes $<'
+ $(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $<
+
+translate/pptacticnew.cmx: translate/pptacticnew.ml
+ $(SHOW)'OCAMLOPT -rectypes $<'
+ $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $<
+
ML4FILES += lib/pp.ml4 lib/compat.ml4
lib/compat.cmo: lib/compat.ml4