From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q48CUVfB012623
	for <caml-list@sympa-roc.inria.fr>; Tue, 8 May 2012 14:30:31 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AmUBAKQRqU/RVdI2kGdsb2JhbABEhXKtKggiAQEBAQkJDQcUBCOCJQIPBBkBGx4DEhAPAiYCJAERAQUBUAeHXQEDC5k7gl4JA4tUUIJzhTEKGScNV4h2AQULgSSMN4IOgRgEiF6NIIERjVE9hA8
X-IronPort-AV: E=Sophos;i="4.75,551,1330902000"; 
   d="scan'208";a="157155612"
Received: from mail-pz0-f54.google.com ([209.85.210.54])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 May 2012 14:30:25 +0200
Received: by dadv36 with SMTP id v36so2821659dad.27
        for <caml-list@inria.fr>; Tue, 08 May 2012 05:30:24 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=mime-version:date:message-id:subject:from:to:content-type;
        bh=4am5aNUF9GnC4y87g9yn8TdUJeY0WRkQfHOiTZQIu3Q=;
        b=Oa6UgxZ5XdggxG6PPQcZ0qDFddIlTsFWxWChrB7Ve5plxEjaYtsMD8ev8pLtt5PWx/
         3evgMvS1gID2KJE8GaF+riDuYsTwAT5bd2V+3ywxMG04MlnUwgM6qG0f1Izbdwm8u+5l
         4K46JeEed2LiOFQJkeFY/jndCzBR8Wm7pr8XvEC7hAPa4/HF4wXWzAlG+EOb9+tn3vDD
         KUuIGRcCklu7V0aVgH12hVy65fbIDXSDezZaHQzu0OwTQPgAFTxK6KHtTzHx14i/UcZc
         O6GMkhZw5yDZxa3CxAPe+INoNlvqpfRS6l/U5IJ6tM20OqWjRuujYohXMz76i/CbpiTr
         0ChQ==
MIME-Version: 1.0
Received: by 10.68.227.37 with SMTP id rx5mr6892665pbc.121.1336480224219; Tue,
 08 May 2012 05:30:24 -0700 (PDT)
Received: by 10.66.46.175 with HTTP; Tue, 8 May 2012 05:30:24 -0700 (PDT)
Date: Tue, 8 May 2012 15:30:24 +0300
Message-ID: <CAPi0vKVSpEPdFGL55JFRa=qcVG_ot4U74-R1_LHQVs81Pb5rpQ@mail.gmail.com>
From: Dmitry Grebeniuk <gdsfh1@gmail.com>
To: caml-list@inria.fr
Content-Type: text/plain; charset=UTF-8
Subject: [Caml-list] ocamlbuild + Coq

Hello.

  Has anybody tried to compile OCaml + Coq project with ocamlbuild?
Maybe you can share myocamlbuild.ml rules for such compilation?
(I already wrote simple rule on "%.v" -> "%.ml", but dependencies'
discovering is killing me, so I'm asking here, maybe there are some
ready solutions.)

  I know about coq_makefile, but I don't want to pollute source tree with
intermediate extraction results.  I could ignore/remove .vo/.glob files,
but Coq extracts some .ml files from his stdlib, so I see no sane way
to ignore some .ml files while not-ignoring other .ml files.