---
name: "o2v"
section: "1"
platform: "linux"
package: "coqprime-tools"
version: "8.20.1-1+b4"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/o2v"
---

# o2v(1)

convert a primo certificate into a Coq proof

## 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