coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert

From: guninski AT guninski.com
To: coq-club AT inria.fr
Subject: Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert
Date: Wed, 4 May 2011 11:02:59 +0200

you are welcome to europe.

btw, strange wording your team has:

$coqc fib6

Error while reading ./fib6.v:
File "/home/joro/prim/fib6.v", line (approx) $z$, characters (approx) $x$-$y$:
Anomaly: uncaught exception Sys_error "/home/joro/prim/fib6.v: $censored$
Please report.

i would bet i can |cat| the file ;)

Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert, guninski
- <Possible follow-ups>
- Re: Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert, guninski
  - Re: Re: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert, Andreas Bogk
  - Message not available
    - Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert, Bruno Barras