The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
In coqtop, if you want see the proofterm behind the lemma "trivial", you
query it by the command Print trivial.
But, in Coqide, the buffer is supposed to be a .v script that you'll
store on the disk and compile. If you write a query here, it will be
executed every time you process or compile the script and this is
(except in the context of teaching) probably not what you want.

There is therefore a "query pane" (that is opened by the shortcut "F1")
to write down queries you want to do once. Moreover, in the case of
Print, you can highlight an occurence of "trivial" in your file and
press "F4" instead of writing Print foo. in the script, proccessing the
line, undo, erase the line <troll>These archaic 4 step ways of querying
something of setting up something once remains so that emacs users stay
happy in their efficient editors :-) (I know, the time I found my mouse
to select the pane, real coders have done the 4 steps and beyond (I
re-know, there are shortcuts for that in Proof general)) </troll>

This is what this warning is willing to say.

Pierre B.

On 01/09/2014 14:38, Michel Levy wrote:
> I am working with coqtop and coqide with version 8.4pl3 (January 2014)
> With coqide and the commands
> Theorem trivial :forall P:Prop,P->P.
> Proof.
> intros.
> exact H.
> Qed.
> Print trivial.
> The last command gives this strange message :
> Warning: query commands should not be inserted in scripts
> trivial = fun (P : Prop) (H : P) => H
>      : forall P : Prop, P -> P
> 
> With coqtop, I have not this message.
> 
> -- 
> email : 
> michel.levy1948 AT gmail.com
> http://membres-liglab.imag.fr/michel.levy 
>