The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Done.

D.

> Would you mind reporting at https://github.com/coq/coq/issues ?
> 
> Thanks!
> 
> Maxime.
> 
> On 02/15/2018 02:17 PM, Dominique Larchey-Wendling wrote:
>> Hi all,
>>
>> Maybe this is a feature but the following example shows a
>> Let Fixpoint construct leaking out of a Section. Is this the
>> desired behaviour (tested under 8.6 and 8.7.1) ?
>>
>> (****************************)
>>
>> Section visibility.
>>
>>   Let Fixpoint ev n := match n with 0 => true  | S n => od n end
>>       with     od n := match n with 0 => false | S n => ev n end.
>>
>>   Let Fixpoint ev' (n : nat) : bool
>>   with         od' (n : nat) : bool.
>>   Proof.
>>     exact (match n with 0 => true  | S n => od' n end).
>>     exact (match n with 0 => false | S n => ev' n end).
>>   Defined.
>>
>>   Let my_even := ev.
>>
>> End visibility.
>>
>> Check ev'.        (* succeeds (unexpected) *)
>> Check my_even.    (* succeeds as expected *)
>> Check ev.         (* fail as expected *)
>>
>>
>> (****************************)
>>
>> I do not see why ev & ev' are treated differently?
>>
>> Thx in advance,
>>
>> Dominique
>>