The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

To answer your actual question, even if perhaps not your intended one, you can pass `-noinit` to Coq and then do `Require Coq.Init.Prelude`, and then everything will need to be qualified.  There isn't a good way to import just some things and not others, though there's a pull request to add this feature at https://github.com/coq/coq/pull/11820

On Mon, Mar 30, 2020 at 8:04 PM Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de> wrote:

Both tricks are very nice.

Thanks
Maximilian

On 30/03/2020 11:25, Christian Doczkal wrote:
> Another possible trick is:
>
> Definition I := I.
>
> Fixpoint test (I : nat) : nat :=
>   match I with
>   | 0 => 0
>   | S I => test I
>   end.
>
> This way, "I" can freely be used as a pattern variable while still being
> convertible to "Logic.I"
>
> Best,
> Christian
>
> On 3/27/20 11:39 AM, Laurent Thery wrote:
>>
>> One possible trick is :
>>
>> Fixpoint test (I : nat) : nat :=
>>   match I with
>>   | 0 => 0
>>   | S (_ as I) => test I
>>   end.
>>
>>
>> On 3/27/20 11:14 AM, Maximilian Wuttke wrote:
>>> Fixpoint test (I : nat) : nat :=
>>>   match I with
>>>   | 0 => 0
>>>   | S I => test I
>>>   end.