diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-07 16:44:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-07 16:44:41 +0000 |
| commit | b3e6d156fbc13ae6d79075265fc20f8912c520da (patch) | |
| tree | 79c3ad02e708da07c70b10b6eccb97e6c2137c88 /Makefile | |
| parent | f2da732ffd5db2b93a2c8120c668f8b2f6068d3b (diff) | |
link Dhyp et Auto
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@221 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -96,7 +96,6 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \ tactics/wcclausenv.cmo tactics/tacticals.cmo tactics/tactics.cmo \ tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo -# tactics/dhyp.cmo tactics/auto.cmo TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \ @@ -104,11 +103,13 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo \ toplevel/usage.cmo toplevel/coqinit.cmo toplevel/coqtop.cmo +HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo + CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ - $(PROOFS) $(TACTICS) $(TOPLEVEL) + $(PROOFS) $(TACTICS) $(TOPLEVEL) $(HIGHTACTICS) CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) ########################################################################### @@ -123,7 +124,7 @@ coqtop: $(COQMKTOP) $(CMX) $(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop coqtop.byte: $(COQMKTOP) $(CMO) Makefile - $(COQMKTOP) -top -notactics $(BYTEFLAGS) -o coqtop.byte + $(COQMKTOP) -top $(BYTEFLAGS) -o coqtop.byte # coqmktop @@ -141,6 +142,7 @@ scripts/tolink.ml: Makefile echo "let proofs = \""$(PROOFS)"\"" >> $@ echo "let tactics = \""$(TACTICS)"\"" >> $@ echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@ + echo "let hightactics = \""$(HIGHTACTICS)"\"" >> $@ beforedepend:: scripts/tolink.ml |