diff options
| author | filliatr | 1999-12-07 16:44:41 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-07 16:44:41 +0000 |
| commit | b3e6d156fbc13ae6d79075265fc20f8912c520da (patch) | |
| tree | 79c3ad02e708da07c70b10b6eccb97e6c2137c88 | |
| 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
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 3 |
2 files changed, 7 insertions, 4 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 diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index bde07410ac..55594d705f 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -48,6 +48,7 @@ let gramobjs = ["g_zsyntax.cmo"; "g_natsyntax.cmo"] let notopobjs = gramobjs (* 5. High-level tactics objects *) +let hightactics = split_cmo Tolink.hightactics let cmotacsobjs = [ "prolog.cmo"; "equality.cmo"; "inv.cmo"; "leminv.cmo"; "point.cmo"; "progmach.cmo"; "program.cmo"; "propre.cmo"; @@ -97,7 +98,7 @@ let module_of_file name = let files_to_link userfiles = let dyn_objs = if not !opt then dynobjs else [] in let command_objs = if !searchisos then coqsearch else [] in - let tactic_objs = if !notactics then [] else cmotacsobjs in + let tactic_objs = if !notactics then [] else hightactics in let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ tactic_objs @ |