Proof Development for Buchberger

The archive of vernacular files (Coq v6.2.4)

Getting the certified code to compute Gröbner bases