From 4759f60b04a278ecd46c8a120340ba55b185c6d1 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 16 Dec 2013 17:08:46 +0100 Subject: A few fixes to the build system (mostly for ocamlbuild) * vars.mli was mentionning Term instead of Constr, leading to a dep cycle * Having a file named toplevel/toplevel.ml isn't a good idea when we also have a toplevel/toplevel.mllib that ought to produce a toplevel.cma. We rename toplevel.ml into Coqloop.ml * Extra cleanup of toplevel.mllib : - Ppextra isn't anywhere around (?!) - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway - Vernacexpr is a .mli and shouldn't appear in an .mllib * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml) * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread for coqchk). --- kernel/vars.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/vars.mli') 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 } *) -- cgit v1.2.3