coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] import

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] import
Date: Mon, 21 Sep 2020 12:47:24 -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 mta03.in.vera.com.uy A931B22312D
Ironport-phdr: 9a23:V2fRWh+/OQ5/9f9uRHKM819IXTAuvvDOBiVQ1KB20u4cTK2v8tzYMVDF4r011RmVBNqdsqgP2rKe8/i5HzBZv9DZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sAfcutMLjYd8Jao8zgfFqWZMd+hK2G9kP12ekwv968uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjeazTfdQaRXBaUcZQSiNOH52zb40NAeUcJ+ZTso3xqlsSoReiAAWhAv7kxD1ViX/sxaA03eQvHx/F0gMiAtwBv2jbrNTpNKoJS++50LXHwi7fY/9K3zr29YjGcgomofGJRb9+a9DeyVU1FwPEklqQqJbqNC6P2OsTqWiU9fZgVf6oi2U6rAxxuiOvxt8yhYnTnI0V1kzE9SJizYYrO9K4UlR0bcS4H5tXsiGWLZZ2Q8M7TmxupS00yaUGtIalcCQW1Jgr3RHSZ+Cdf4WG/x7vTvudLDZgiH54er+zmQy+/Vavx+HmWMS4zUxGoyRYntTKq3sD1xvT6tKcRft840iuxCiA1wbR5O5ZO0A5jaTVJZ4/zLAzlJUdrEvMETP3mEXql6KZbFko9fSz5Oj7frnqvpGSOY9qhA/9MKsgh8OwDvg5MggSRGWU4/iw26H48kHlXLlHiOA9nLPDv5DAP8sbo7a0Aw9L3YYn7BayFzKm384ZnXkDNl5FZgyIj5LzNF3UPP/4CvK/j06xkDZr3/zGP7vhDYvRLnXbjrvtYapx51RTxQYv19xS6Y9YBqscLP/yQkPxscbXDh49Mwy62ebnD9B925sGWWKUGq+WLrnSvkWU5uIzJOmBf5EVtyjnK/c//fLhkXg5mVoHcam03ZobcGq4Eeh+I0WFfXrshc8MHnsNvgonVeDllFmCUSNIaHupRKI95jQ7CJq8AovZR4CthqaB3CahEZFMaGBGEAPELXC9fIKdHvwIdSjadsRmi3kPUaWrY44nzxCn8gHgnelJNO3RrxURqYji39l8r9Xejxgu6Ts8W9yGy2yXRn1omUsWSiU/mqt4pApg2wHQguBDn/VEGIkKtLtyWQAgOMuBl7QjWoLCHznZd9LMc26IB9CvADU/VNU0moRcfUtnEpOpiRWFwjv4WuZJxYzOP4Q99+fn51a0P9x0ki2UyqQ7hh8tRc4JKHz03vcipTiWPJbAlgCir4jvdakY23edpmKKzG7IokxCWUh7VqCDQGFNPkY=

I have defined some proofs in a file .v and I want to import

it inside other file in the same folder.

How can I do this?

Regards,

Patricia

[Coq-Club] import, Patricia Peratto, 09/19/2020
- Re: [Coq-Club] import, Pierre Courtieu, 09/22/2020
  - Re: [Coq-Club] import, Théo Zimmermann, 09/22/2020
    - Re: [Coq-Club] import, Erik Martin-Dorel, 09/22/2020
- <Possible follow-up(s)>
- [Coq-Club] import, Patricia Peratto, 09/21/2020