The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

Coq sometimes prints terms in such a way that they cannot be parsed again.  
This is irritating when you learn Coq and also ruins some examples I would 
like to use when teaching proof terms.  The problem is with type inference.  
Here is an example.

Definition L : true <> false :=
   fun A => eq_ind_r (x := false) (fun b => if b then False else True) I A.

Print L.

(* fun A : true = false =>
      eq_ind_r (fun b : bool => if b then False else True) I A *)

Check fun A : true = false =>
         eq_ind_r (fun b : bool => if b then False else True) I A.

(* Error blah blah *)

This is run with Coq 8.4.  The problem persists in Coq 8.5

I would hope that printing terms such that they can be parsed is a design 
goal.

Gert