From ddc83ed89cd6671cfa6b5bf2d0ce1fb74ad206c1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 17 May 2005 12:43:22 +0000
Subject: Extension de Tactic Notation pour permettre d'tendre et de faire
 rffrence aux niveaux syntaxiques des tacticielles

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'Makefile')

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
-- 
cgit v1.2.3