The zip file should contain six coq script files.  The first two files
require no file outside the standard library of Coq.  The first two files
can be run in Coq version 8.4pl3 and later.

The next 4 files require coquelicot-2.0.0 and ssrflect-1.4.

rounding_big.v
	This file can be compiled with only the standard library of Coq, it
	describes functions to compute large numbers of digits of pi, but does
	not perform any computation.
computing.v
	This file only loads the previous file and launches the computation.
	This file contains the computation of one thousand digits of PI.
	The computation of one million digit is also described, but the line
	is commented out.  It can be run only in a version of Coq that supports
	native_compute (the development version, for instance, in December 2014).
agm.v
	This file contains all the axioms corresponding to the proof of
	mathematical correctness for the sequence of real numbers that
	approximates pi, based on arithmetic geometric means.  These axioms
	are actually proved in another development, not given here.
log2.v
	This file contains a description of the logarithm function, computed
	in the fixed precision setting described in the paper
	"Fixed Precision Patterns for the Formal Verification of
	 Mathematical Constant Approximations"
ln_2_10.v
	This file contains precise information about big powers of 2 and big
	powers of 10, as needed by the correctness proof in the next file.
rounding_correct.v
	This file contains the proof that the computation of one million digits
	is correct.