coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] compiling

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] compiling
Date: Wed, 23 Sep 2020 13:26:00 -0300 (UYT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta01.in.vera.com.uy 109CD221E1F
Ironport-phdr: 9a23:UkRsPhDdwfxAmdijgFKRUyQJP3N1i/DPJgcQr6AfoPdwSPX6o8bcNUDSrc9gkEXOFd2Cra4d1KyP7euxCSRAuc/H7ClcNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULg4ZuMLs9xxrGrnZMeOld2GdkKU6Okxrm6cq84Z9u/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnNTAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhygZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4dSmRBWcZRTTdOAoKhYIQSEeUBO+RWoJTnp1ATqRezBRWgCP/qxjJOm3T437A10/45HA/I3AIuAdEAv3bJotr6KKgSUPy1wbLSwjnfc/xZwivx5JTOfxs8of+MR7Vwcc/JxEc1DQzFkk+QqY35MDOUzOsGrnKV4PR6Ve21l24ntwZxqSWoy8c0kYnJnpwaykre+iVl3IY1Isa1SFBlbt6+CpRcrT2VN4xzQs84XmFpuD83x7sbspC4ZCgH0IorywLDZ/CdfIWE/gjvWeiMLTtii39oeaqziwuw/ES+0OHwSMa53ExEoyZYiNXBuG0B2hrO4caHTft95Fyu2TeS2A/O9O5EJ0I6mrfBK5M5zLA+loQdv0fBESHrl0r5kK6Wdlk/9+ey9+jofq7pqoOAO4NshA/wMroglM+9DuolPQcBQ2mb+fin2bL54UH2XK5FguEqnqTfrZvUP94UprSjDA9Qyosj6wiwDzOh0NkAmHkINlNFeBadg4j3JV7OOur3Ae2jjFSrlTdn3e3GP735DpXMKHjMjqvhcK5j50JA1AY/199S645OBrwPPf7/QED8ud3AAh88KQO0wuLnCNtn1oMZXGKCGreZMLjKsVCW/OIgOfWMZJMSuDvmNfgq+eTugmUjlVABeqmp2IEbaG24H/h+OUWWfWLsgssdEWcNpgcxUOvqiESbXTFPY3ayQrkz6yogCIOmCIfDXpqijKaA3Ce9BJ1WZ3pJBkqCEXfyJM24XKIHbzvXKct8mHRQXr+4DoQlyBuGtQngyrMhIPCCqQMCspe27NFp/ezYlBh6zTFuBtiB1CnZV3psk3kBWyMx9L5yu0U7wVCGl7Vp1a8LXedP7u9EB15pfaXXyPZ3Xo2qAlucLOfMc06vR5CdOR90Tt81xIZeMUN0GtHkkB3Z1myhBLpTiq3ZXMVloJKZ5GD4IoNG81iD0aAgi1c8Rc4Wbj+4i7R2sQPUAsjUghfAzvr4ReEnxCfIsVy74y+WpkgBC1xuXL/MG3sYYw3LvIah6w==

I want to compile a simple file called Ident.v.

I have written the following _CoqProject in

the same folder where I have the Ident.v file.

-R . .
-arg ./Ident.v

when I try to load the file from which I import

Ident.v gives a compilation error message.

I don't know how to write the _CoqProject file.

Can you help me?

Regards,

Patricia

[Coq-Club] compiling, Patricia Peratto, 09/23/2020
- <Possible follow-up(s)>
- Re: [Coq-Club] compiling, Enrico Tassi, 09/24/2020
  - Re: [Coq-Club] compiling, Patricia Peratto, 09/24/2020
    - Re: [Coq-Club] compiling, Pierre Courtieu, 09/24/2020
- [Coq-Club] compiling, Patricia Peratto, 09/25/2020
  - Re: [Coq-Club] compiling, John Zhuang Hui, 09/25/2020
  - Re: [Coq-Club] compiling, Maximilian Wuttke, 09/25/2020