The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

(1) I know that I can take advantage of partial proofs using refine, but can I treat partial proofs as first class values? E.g., I'm trying to do this, but Coq complains that it can't infer the value of the hole.

Definition pair_fun_template: pair_nat_nat -> nat :=

(fun p: pair_nat_nat => 

    match p with mk_pair t u => (_ : nat) end).

(2) When using CoqIDE and literate Coq in the style of Pierce's book, Coq constantly complains, "Warning: query commands should not be inserted in scripts." How can I turn off these warnings?

Thanks!

Kevin