Skip to Content.
Sympa Menu

coq-club - [Coq-Club] definition accepted by coqc but not accepted by coqtop

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] definition accepted by coqc but not accepted by coqtop


Chronological Thread 
  • From: Frederic Blanqui <frederic.blanqui AT inria.fr>
  • To: Coq-Club Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] definition accepted by coqc but not accepted by coqtop
  • Date: Wed, 10 Oct 2012 16:12:17 +0800

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.




Archive powered by MHonArc 2.6.18.

Top of Page