The Coq mailing list

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

2012/10/11 AUGER Cédric <sedrikov AT gmail.com>

Le Thu, 11 Oct 2012 13:09:01 +0800,
Frederic Blanqui <frederic.blanqui AT inria.fr> a écrit :

> 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)?

Top does not refer to the current file, but rather to the current
module.

When using coqtop, your session may not correspond to a file (and
generally it should not, as it is interactive).

True.
 

Coqc on its side relies
on files, I don't think you can use coqc on something which is not a
file.

True but I don't see why this prevents coqc to treat "Top" as coqtop does.

P.

So, they may behave differently, since the environment is
different.

> 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

> > <mailto: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.
> >
> >
>