The Coq mailing list

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

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