The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello.

I have a problem for having both coqc and coqtop accept some definition:

Section S1.
  Variable A : Type.
  Inductive t := c : A -> t.
End S1.

Section S2.
  Variable A : Type.
  Notation c := (c A).
  (* this first definition is not accepted because c is a notation:
  Definition f (x : t A) := match x with c _ => 0 end.*)
  (* this second definition is accepted by coqtop (ProofGeneral) but 
not by coqc:
  Definition f (x : t A) := match x with Top.c _ => 0 end. *)
  (* assuming that this code is put in file.v, then
  this third definition is accepted by coqc but not by coqtop (via 
ProofGeneral):
  Definition f (x : t A) := match x with File.c _ => 0 end. *)
End S2.

Why the second definition is not accepted by coqc?

Is there a definition that can be accepted by both coqc and coqtop, 
while keeping c as a notation for (c A) in section S2?

Thanks for your help.

Frederic.