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: Sat, 19 Sep 2020 15:54:23 -0300 (UYT)
Authentication-results: mail2-smtp-roc.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 C6DD7222052
Ironport-phdr: 9a23:j8bHRRfxYSEFLSLiPmNU9UF3lGMj4u6mDksu8pMizoh2WeGdxcW7Yx7h7PlgxGXEQZ/co6odzbaP7Oa4CSdZucnJ8ChbNsAVCVld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6Q8xgHVrnZLdOha2H9kKFCOlBr4+su84YRv/itNt/8g7cJMTbn2c6ElRrFEEToqNHw46tf2vhfZVwuP4XUcUmQSkhVWBgXO8Q/3UJTsvCbkr+RxwCaVM9H4QrAyQjSi8rxkSAT0hycdNj4263/Yh8pth69Guh2hphh/w4nJYIGJMfd1Y63Qcc8GSWdHQ81eUCxPAoSmb4QUDuoOIPtXoJf7p1UMsBS+HxSnCOfvxzNUmnP62Ks32PkjHw7bxgwtB9wAvnTKotv2NqgcTO+6w7XJzTXfdP5Zwyvx55TTfRw9vf2BW697f8rLyUkoEgPIlk+eppb5PzOP1+QCr2mb4PB9Xuy1lWEnsRt+oiSzxscrl4LEgZoVykvc9Spn2oY6P8G4SFJ8YdO/DptfqTuaOJFsTsw+RGFovTw2yqAGuJOieiUB1ZcpxwbHZvCZb4SE/gjvWemNLTtiin9pZaizihmz/ES41+HxVNe43ExUoidKiNXBuG0B2wbd58SZTPZ240ev2TGV1w/I6+FLPF07mrTdK5Aj37EwjIIev0rDECHom0v5jrKYeUo49eip9+Tqea/pqoOAOIBvlg3yLrwilMK/D+omMQYBXXWV9uug273i4U30W69FguEqnabCrJzWOcIWrbOjDQBPyIYs8RO/Ai+m0NsGmXkHK0pIeBedgIjoP1HCOu74Aumlg1u2ijtk2/fGPrj7DpXQLnnPiLbhfbBj5E5A0Ac/08xT645OBrwOPP7/QEH8uMHCAhI2MgG42+PnB8981oMaV2KPGKiZMKbKvF+Q/eIvO/eDZJUPtzbhN/gl4OXjjWEnll8HZ6alx4cYaHe9Hvh8PkWYYWLggs0dHmcSogo+UOvqhUWeXj5Ufna+Rr4z5jUmCI29ForDXYCsgLmZ3CihBJFWZ2ZGCkqNEXjybYmEVe0MO2quJZpqlSVBXry8Qcd13ha38QT+1rBPL+zO+yReu4i1h/Zv4OiGrRgu7z1/Ds3V62yXRn1omStcXyQu0bp2vVB64kmOy6E+iPtdU8FCsaAaGjwmPILRmrUpQ+v5XRjMK4rREA/3EOXjOik4S5cK+/FLZk98H9u4iRWahHi0DqUc0beMAdop4/CFhiSjF4NG03/DkZIZoRw+WMIWbj+4i7R2sQPUAsjUghfBzvv4ReEnxCfIsVy74y+OsUVfCV4iVKzEWTYBa1Hf69/+4wXfXu32BA==

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

it inside other file.

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