coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e AT x80.org (Emilio Jesús Gallego Arias)
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Makefile targets
- Date: Fri, 15 Dec 2017 17:27:42 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
- Ironport-phdr: 9a23:X6MuMh/VXYY6w/9uRHKM819IXTAuvvDOBiVQ1KB52+gcTK2v8tzYMVDF4r011RmVBdyds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+54Dfbx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaMD45/m/Zhc5zgq1Vrx2uuwdyw5LIbIyPKPZyYrnQcNEcSGFcXshRTStBAoakYoQRFOcAMuVVo5Xnq1sJtxu+ChSnCOfgxD9Nh3/22aw60+M8Gg/CwgMgBMgWsG/Jp9v0LqgSVeS1w7fHzTXEcvhbxS396InSfRA6pP2BW697f8nJyUQ3Cg/IjVadpZb7Mz+L1+kBqXWX4uh9We61lmIqpR99riCsy8otkIXEh4AYxkrA+Clj3Yo4K9u1Q1Nhb9G+CptfrSSaOpN2Qsw8R2Fovz43y7IFtJKnZiQKz44nxxHHZ/yGdYiH/A7jWf6MLTp7h39pYqyziwiz/ES61+HxVNS43ExXoidLjNXArnUN2AbS6siDRPt95ECh2TOX2g/N8exFLkM5mbbBJ54m2L4wmYIfsV7fES/uhEX2kKiWe1049eiv8uTre6npppuBN4BvkQz+KaQvmsmnAesiKAQOXm6b+f691LL550H5Tq9K3bUKlfzSt4mfLsAGrIa4BRVU28At8UWRFTCjhdkwjSlfalVfd1rHoo3oP1DJaNL1FmWky3ullDNmyPeOF6fgC46MfSuLq6voYbsosx0U8wE0190Kv58=
- Organization: X80 Heavy Industries
"N. Raghavendra"
<nyraghu27132 AT gmail.com>
writes:
> I have a Coq development, for which I am using coqtop / coqc with
> the -noinit option, and the commands
>
> Declare ML Module "ltac_plugin".
> Global Set Default Proof Mode "Classic".
> So, is there a set of Makefile targets for building Coq, which gives
> me just coqbinaries, tools, and the ltac plugin?
Well, if you wanna be so fine grained I think you may want to use directly:
$ make plugins/ltac/ltac_plugin.cmxs
etc...
E.
- [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Gaëtan Gilbert, 12/15/2017
- Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Emilio Jesús Gallego Arias, 12/15/2017
- Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Gaëtan Gilbert, 12/15/2017
- Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Emilio Jesús Gallego Arias, 12/15/2017
- Re: [Coq-Club] Makefile targets, Gaëtan Gilbert, 12/15/2017
- Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Gaëtan Gilbert, 12/15/2017
Archive powered by MHonArc 2.6.18.