diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-16 19:05:27 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-07-16 19:05:27 +0000 |
commit | 3e430c449809e6db5c20c2b5b57fafdd5a230fd3 (patch) | |
tree | 29797387c1c2c33628c08409fe628a2ed93d6241 | |
parent | 3202711c3197f02dd498fbe9f018d1f12b74de7a (diff) |
Suppression quotify
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5918 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile | 17 |
1 files changed, 1 insertions, 16 deletions
@@ -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 \ |