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 /scripts/coqmktop.ml | |
| 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 'scripts/coqmktop.ml')
| -rw-r--r-- | scripts/coqmktop.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 @ |