diff options
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | _tags | 4 | ||||
| -rw-r--r-- | kernel/vars.mli | 2 | ||||
| -rw-r--r-- | myocamlbuild.ml | 8 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 1 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 18 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 | ||||
| -rw-r--r-- | toplevel/coqloop.ml (renamed from toplevel/toplevel.ml) | 0 | ||||
| -rw-r--r-- | toplevel/coqloop.mli (renamed from toplevel/toplevel.mli) | 0 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 2 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 6 |
12 files changed, 15 insertions, 33 deletions
diff --git a/Makefile.common b/Makefile.common index b13e828c4..d41fc909d 100644 --- a/Makefile.common +++ b/Makefile.common @@ -156,7 +156,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ - printing/printing.cma parsing/parsing.cma tactics/tactics.cma \ + parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma @@ -9,10 +9,10 @@ <tools/coq_makefile.{native,byte}> : use_str, use_unix <tools/coqdoc/main.{native,byte}> : use_str <ide/coqide_main.{native,byte}> : use_str, use_unix, ide -<checker/main.{native,byte}> : use_str, use_unix +<checker/main.{native,byte}> : use_str, use_unix, thread <plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix <tools/mkwinapp.{native,byte}> : use_unix -<tools/fake_ide.{native,byte}> : use_unix +<tools/fake_ide.{native,byte}> : use_unix, use_str ## tags for ide diff --git a/kernel/vars.mli b/kernel/vars.mli index a61482d0e..a09265036 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Context (** {6 Occur checks } *) diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 5a03470a4..9a062220a 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -105,7 +105,7 @@ let _build = Options.build_dir let core_libs = ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; - "printing/printing"; "parsing/parsing"; "tactics/tactics"; + "parsing/parsing"; "printing/printing"; "tactics/tactics"; "toplevel/toplevel"; "parsing/highparsing"; "tactics/hightactics"] let core_cma = List.map (fun s -> s^".cma") core_libs let core_cmxa = List.map (fun s -> s^".cmxa") core_libs @@ -301,7 +301,7 @@ let extra_rules () = begin (** All caml files are compiled with +camlp4/5 and ide files need +lablgtk2 *) - flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4incl]); + flag ["compile"; "ocaml"] (S [A"-thread";A"-rectypes"; camlp4incl]); flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]); flag ["ocaml"; "ide"; "compile"] lablgtkincl; flag ["ocaml"; "ide"; "link"] lablgtkincl; @@ -389,9 +389,9 @@ let extra_rules () = begin if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]) in if opt then rule fo ~prod:fo ~deps:(depsall@depso) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;camlp4incl;A"-o";Px fo]); + (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;A"-thread";camlp4incl;A"-o";Px fo]); rule fb ~prod:fb ~deps:(depsall@depsb) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;camlp4incl;A"-o";Px fb]); + (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;A"-thread";camlp4incl;A"-o";Px fb]); in (** Coq files dependencies *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ba640863d..4ece6cb24 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -9,7 +9,6 @@ open Pp open Names -(* open Compat *) open Errors open Util open Extend diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index 0e6eba267..a3d0465a6 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -6,22 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Genarg -open Vernacexpr -open Names -open Nameops -open Nametab -open Ppconstr -open Pptactic -open Glob_term -open Pcoq -open Libnames -open Ppextend -open Topconstr - (** Prints a vernac expression *) -val pr_vernac_body : vernac_expr -> std_ppcmds +val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds (** Prints a vernac expression and closes it with a dot. *) -val pr_vernac : vernac_expr -> std_ppcmds +val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds diff --git a/printing/printing.mllib b/printing/printing.mllib index 9b3bffc8d..2a8f1030f 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -5,3 +5,4 @@ Printer Pptactic Printmod Prettyp +Ppvernac diff --git a/toplevel/toplevel.ml b/toplevel/coqloop.ml index 3bcf935cc..3bcf935cc 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/coqloop.ml diff --git a/toplevel/toplevel.mli b/toplevel/coqloop.mli index 1375f3361..1375f3361 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/coqloop.mli diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a0de42bf6..68f58e666 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -401,7 +401,7 @@ let init arglist = if !batch_mode then mt () else str "Error during initialization:" ++ fnl () in - fatal_error (msg ++ Toplevel.print_toplevel_error any) + fatal_error (msg ++ Coqloop.print_toplevel_error any) end; if !batch_mode then begin flush_all(); @@ -425,7 +425,7 @@ let start () = else if !Flags.coq_slave_mode > 0 then Stm.slave_main_loop () else - Toplevel.loop(); + Coqloop.loop(); (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 73e214849..ee511edbb 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -9,7 +9,7 @@ (** The Coq main module. The following function [start] will parse the command line, print the banner, initialize the load path, load the input state, load the files given on the command line, load the ressource file, - produce the output state if any, and finally will launch [Toplevel.loop]. *) + produce the output state if any, and finally will launch [Coqloop.loop]. *) val init_toplevel : string list -> unit diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index ab8c89623..0ad82abd3 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -2,9 +2,6 @@ Himsg Cerrors Class Locality -Vernacexpr -Ppextra -Ppvernac Metasyntax Auto_ind_decl Search @@ -15,7 +12,6 @@ Obligations Command Classes Record -Ppvernac Vernacinterp Mltop Vernacentries @@ -24,7 +20,7 @@ Stm Whelp Vernac Ide_slave -Toplevel Usage +Coqloop Coqinit Coqtop |