coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Makefile targets

From: "N. Raghavendra" <nyraghu27132 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Makefile targets
Date: Sat, 16 Dec 2017 00:26:17 +0530
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nyraghu27132 AT gmail.com; spf=Pass smtp.mailfrom=nyraghu27132 AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f177.google.com
Ironport-phdr: 9a23:fHa2BB8Hrt5OL/9uRHKM819IXTAuvvDOBiVQ1KB32+McTK2v8tzYMVDF4r011RmVBdyds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+54Dfbx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaNTE5/m/YitZ+gqxYrx2uuxNxzpXIYIGMLvdyYr/RcMkYSGdHQ81fVzZBAoS5b4YXAeYPJfxUpJThqVQUohu+BROjBP3xxT9Om3D2x7c13+o8GgzB2gwhH8gOv27brNX1KaceT+K4wLTGwDnddP5W1jL955LJchAlu/2DQbVwcc/IxEQpCgjLgFKQqYn/MDOU0OQAq3ab7+16WeKul24rswFxoiKuxss2kInGmJkVxkrF9SV/2Io1P8O3SFJhYd6jDJtfqS6bN5dtQs84RWFnpjo6x7sbspC4ZCgH0IorywLbZvCdcIWF4gjvWPuVLDtmnn5pZbCyihSq/US+1OHwStO43EhUoidHiNXAq2wB2hLJ5sSaRPZw/EGs0iuV2Q/J8OFLO0U0mLLbK5E/xr4wkYIesUHZES/3nEX6lbeWdks49uSx5eTrf7frq52GO497jQH+NasumsihDugiLgcOWG2b9fy91L3l40L5XK1HguMqnqTdqpzXJsQWqrSkDwJRzIov8QuzAjWk3dgAmHkINlNFeBaJj4jzPFHOJej1DfG/glS2ijhryPDGPqD/DpjPM3TOnqntcK1y605Z0gUzzNRf64hIBbEGJfL/QlXxu8DADh8lLwy0xP7qB8l61oMHQG6AHquZML7JvlKT/eIuI+yMZJcPtzrnKvgl4eTujX4jllMHc6mpx8hfVHftFfN/Zk6dfHDEg9EbEG5MsBBtduHyjEy+VmsZQTD6Zasz5jglBYSqF46JDtSrkaaI0yemRMIPPTpuBVWFEHOufIKBDaQiciWXd4VH1HQ+XLehQpEs0x20vUWyn7x2NOPb+jBC6su4jvB64uTSkVc58jkiXJfV6H2EU2whxjBAfDQxxq0q+UE=

At 2017-12-15T19:45:18+01:00, Gaëtan Gilbert wrote:

> Coq checks that a path has the Coq stdlib by checking for the
> Prelude.vo. It does this check even with -noinit. I would say
> (although it's debatable) this isn't a bug because the stdlib is also
> where the cmxs lives so without it
>
> Declare ML Module "ltac_plugin".
>
> won't work.

Thanks, that explains the error I was getting.

Best regards,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[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