The Coq mailing list

[Michel Levy <michel.levy1948 AT gmail.com>]

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