coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Patricia Peratto <psperatto AT vera.com.uy>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] compilation
- Date: Tue, 22 Sep 2020 16:16:33 -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 mta02.in.vera.com.uy 1068B2224AC
- Ironport-phdr: 9a23:aLTxFx0b8BSfGrkfsmDT+DRfVm0co7zxezQtwd8ZseIQI/ad9pjvdHbS+e9qxAeQG9mCtLQd16GP6PqoGTRZp8rY7jZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq8sbjZF/Jqs+xRfFv3VFd/pLzm9sOV6fggzw68it8JNi6Shcp+4t+8tdWqjmYqo0SqBVAi47OG4v/s3rshfDTQqL5nQCV2gdjwRFDQvY4hzkR5n9qiT1uPZz1ymcJs32UKs7WS++4KdxSR/nkzkIOjgk+2zKkMNwjaZboBW8pxxjxoPffY+YOOZicq7bYNgXQ3dKUMRMWCxbGo6yYYsBAfQCM+laoYnzulQBoge/BQmwH+7g0CNEiWPt0qEmz+gsEwfL1xEgEdIUt3TUqc34Or0IXuCp1qnIzCnMb/JM1jzg8obHbAohruuQXbJsdsra1E4iFxvejlWIt4PlJSma1vgRs2ic9OdgS/ygi3Q9pA1rvjevwcIshpPUhoMV013J8zhyz4kpK9OiUkF7fcKkH4VKtyGcL4Z7TcwvTmNntis7yrMKpIC3cigKxZkjxhPSaPyKfoyI7B//WuicIil0iG9hdb+jhRu/8EitxO38W8Wo31tGszdIn9/RvX4Ozxze8taLRudh8ku71juDyxrf5+9ZLUwumqfWKoYtzqMym5YNq0jPACD7lF/4gaOLbEkp9PSk5uL6abv8vJCcLZV7igTmP6QuhMO/BeM4PxALX2eB+OS80Kfv/VPnT7VQlPI6iLXWsJffJcgBu664AxdZ0ocl6xmhEzeryMoUkWUbIF5fdx+Lk5LlNl/TLPziAvqygkygkDJxyPDHOr3hDI/NLn/GkLr5ZbZ98FZcxxQpzd9F+5JUFrYBLentWkDvrtzXFAU1PBCzw+biEtl9y4MfVXqVAqCFKKPSrUOI5uU3LuaQY48VoS/xJOQh5/7zlnA0gkQdfKms3ZsPcn+0BPVmI0ODYXrtmNgNC2kKvhBtBNDt3VaFSHtYY2u4F/Y34Sh+A4a7B6/CQJqsifqPxnHoMIdRYzV+A0yWEHzpfs28Vu0FdD6Vapt5iSQJT7G9V4gJyxy0vUnxzL8hM/uCqX5Qjo7qyNUgv76brho17zEhV53AgVHIdHl9myYzfxFz3K17phUtmFKK0Kw+nfFCHJpY4PYPTxZobceNndw/MMj7X0f6RvnMTV+nRtu8BjRoFYAvzsUHJU16HpO/n0Kahnb4M/ouj7WOQacM3OfExXGofJRjxmzPkqImih87U5kXOA==
The question is if is correct the way I have compiled.
The command coqc didn´t work. Shows a definition
inside the file.
In what respects to use the file that has adjoined Erik I
don't know which name I have to give to the file and
in which folder I have to put it.
Regards.
Patricia
- [Coq-Club] compilation, Patricia Peratto, 09/22/2020
- Re: [Coq-Club] compilation, Patricia Peratto, 09/22/2020
Archive powered by MHonArc 2.6.19+.