The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 04/24/2014 05:39 PM, Arnaud Spiwack wrote:
> > Is it strange at all then that I can get IList.v through the type checker
> > without using -impredicative-set, including the recursor and induction?
>
> Are you using Proof General to run the file ? If so, the first line of the
> file:
>
>   (* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)
>
> automatically passes the -impredicative-set flag to Coq.

OK - I see that by restarting emacs after removing that mode line, the 
setting goes away, and now IList fails immediately.

-- Jonathan