coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to make local sources take precedence over the library?

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to make local sources take precedence over the library?
Date: Tue, 3 Sep 2019 18:34:41 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f68.google.com
Ironport-phdr: 9a23:SwOskhzam+SEi7LXCy+O+j09IxM/srCxBDY+r6Qd2+oUIJqq85mqBkHD//Il1AaPAdyBrasb0KGJ6ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVmjaxe65+IRe4oAnetMQanJZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLzliwJKyA2/33WisxojaJUvhShpwBkw4XJZI2ZLedycr/Bcd8fQ2dKQ8RfWDFbAo6kYIQPAegOM+ZWoYf+ulUAswexCwa3CePz0z9FnGP60bEm3+kjFwzNwQwuH8gJsHTRtNj7KqcSVvqyzKbQzjrDbvZW2TLj54jSdxAuu/eMXbRtesfW1UkvFx3KjlKKpY3kPjOV0+ENs2mA4upvUOKgkW8nqwVrrjezwccsj5DEi4QIwV7K8iV5xZw6Jdy+SENjYN6kFoFQtyCAOIdsTMMiWWdlszs5xL0eoZO3YjQGxZA9yxPca/GLaZaE7g/hWeqLIDp1h3Roc6+liRmo60iv0Oj8W9G00FlUqipFlcHBtnUX2BzS7siLU+V9/ly81TqW2QDe6+JJLVo7larcLJ4hzbowmYQJvUvfGS/2nV36jK6Qdko65uil8/rrbqniq5OGNIJ5ihvyProzlsG9G+g1MwsDU3Ce+eum1b3j+UP5QK9Njv0ziqTZrJDaKtocpqKjAg5V04Mj6xO+Dzq939QYmGMILFNBeB6dk4fpPFTOLOjiDfijm1SsjCtrx/feM7L9BZXNN2HPn6vlfbZg8EFR0xEzzNBa55JMEL4NOvPzWknrtNzZFBA1KQK0w/y0QOl6g6gZQCqkBrKTePfZtkbN7eYyKcGNYpUUsXDzMa52yeTpiCoFmd4aSpuo2J4acnWxGPIud1mZbH2qkNYEFGYisQ83Teisg1qHB20AL02uVr4xs2loQLmtCp3OE8X02OTYgXWLW6ZOb2UDMWiiVHflc4LeBqUJYSOWZ9F6y3kKC+jnRIgm2hWj8gT9zug/d7aGymgjrZvmkeNNyajLjxhrrG57Cs2c1yeGSGQmxjpZFQ9z57h2pAlG8nnG1KF5h/JCEtkKvqFGVw47MdjXyOkoUt0=

Hi,

If the collision occurs at Require Import time, you can use the From
prefix to specify that the module should be found in your own project
instead of Coq's library.
Cf.
https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmdv.require-import

Théo

Le mar. 3 sept. 2019 à 18:31, Karl Crary
<crary AT andrew.cmu.edu>
a écrit :
>
> Hi all,
>
> I upgraded to 8.9.1, and found that several new modules have been added
> to the library whose names collide with my own. Unfortunately, this
> breaks my code in many places. Is there a way to tell Coq to give
> precedence to local sources over libraries?
>
> Thanks for any help.
>
> -- Karl Crary
>

[Coq-Club] How to make local sources take precedence over the library?, Karl Crary, 09/03/2019
- Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/03/2019
  - Re: [Coq-Club] How to make local sources take precedence over the library?, Karl Crary, 09/03/2019
    - Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/03/2019
      - Re: [Coq-Club] How to make local sources take precedence over the library?, Maxime Dénès, 09/04/2019
        
        Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/04/2019
      - Re: [Coq-Club] How to make local sources take precedence over the library?, Robbert Krebbers, 09/04/2019
        
        Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/04/2019
    - Re: [Coq-Club] How to make local sources take precedence over the library?, Pierre Courtieu, 09/04/2019