aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-07-16 19:05:27 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-07-16 19:05:27 +0000
commit3e430c449809e6db5c20c2b5b57fafdd5a230fd3 (patch)
tree29797387c1c2c33628c08409fe628a2ed93d6241
parent3202711c3197f02dd498fbe9f018d1f12b74de7a (diff)
Suppression quotify
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5918 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile17
1 files changed, 1 insertions, 16 deletions
diff --git a/Makefile b/Makefile
index c2e52b421..949d03dbb 100644
--- a/Makefile
+++ b/Makefile
@@ -84,7 +84,7 @@ DEPFLAGS=$(LOCALINCLUDES)
OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS)
OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
-CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo
+CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo
CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p'
COQINCLUDES= # coqtop includes itself the needed paths
@@ -204,21 +204,6 @@ HIGHTACTICS=\
tactics/autorewrite.cmo tactics/refine.cmo \
tactics/extraargs.cmo tactics/extratactics.cmo tactics/eauto.cmo
-QUOTIFY=\
- parsing/qast.cmo parsing/q_prim.cmo parsing/q_tactic.cmo
-
-parsing/q_prim.ml4: parsing/g_prim.ml4
- $(SHOW)'CAMLP4O -o $@'
- $(HIDE)camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_prim.ml4 -impl parsing/g_prim.ml4
-
-parsing/q_tactic.ml4: parsing/g_tactic.ml4
- $(SHOW)'CAMLP4O -o $@'
- $(HIDE)camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_tactic.ml4 -impl parsing/g_tactic.ml4
-
-parsing/q_ltac.ml4: parsing/g_ltac.ml4
- $(SHOW)'CAMLP4O -o $@'
- $(HIDE)camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_ltac.ml4 -impl parsing/g_ltac.ml4
-
SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4
USERTAC = $(SPECTAC)
ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \