NAME

       o2v - convert a primo certificate into a Coq proof

SYNOPSIS

       o2v [-split] [-n theorem] [-o filename] primocertif

DESCRIPTION

       This  tool  takes  a certificate file generated by primo (https://ellipsa.eu) and turns it
       into a Coq proof script.

OPTIONS

       -split Generate one proof by certificate in the primo file

       -n <theorem>
              Name of the final theorem in the Coq proof

       -o <filename>
              Prints the proof script in the file named <filename> (otherwise: FirstPrimes.v)

       <primocertif>
              Name of the primo certification file

                                         July 15th, 2022                                   O2V(1)