The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi, the final try is probably the good one but you should call coqtop like this: "coqtop -top File".

In proofgeneral you can put this at the end of the file to store the right invocation of coqtop:


(* Local Variables: *)
(* coq-prog-args: ("-emacs" "-top" "File") *)
(* End: *)

Hope this helps.

P

2012/10/10 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.