The Coq mailing list

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

Thanks Pierre!

Yet, we could imagine that, even in coqc, Top denotes the current file. From the point of view of Coq developers, is there any reason for not doing that (and having coqtop and coqc behave differently)?

Regards,

Frederic.

Le 10/10/2012 16:52, Pierre Courtieu a écrit :

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.