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).
---
 _tags | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to '_tags')

diff --git a/_tags b/_tags
index 5bb8564801..8cb8b1f90e 100644
--- a/_tags
+++ b/_tags
@@ -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
 
-- 
cgit v1.2.3