# CoqInE

## Update:

Ali Assaf is working on a new implementation of Coqine with support for type universes. You can find it at the InriaForge project here, in the `develop`

branch.

Also check out Krajono project, a translation of Matita proofs to Dedukti.

## What is CoqInE?

CoqInE permits to produce Dedukti proofs from Coq proofs. It is developed by Mathieu Boespflug, Guillaume Burel and Quentin Carbonneaux.

## Get CoqInE

Download this file. Unzip and extract it

tar xvzf coqine.tar.gz

Change directory

cd coqine

Make sure you have
OCaml
installed or install it. Make sure you have
have Coq installed (in order to be
able to generate `.vo`

files used by CoqInE, using
the `coqc`

command). Warning: the version of OCaml used to
compile CoqInE must be the same as the one used to compile the Coq
program that generates the `.vo`

files you want to
translate.
Make sure you have
Dedukti
installed or install it.

Then configure and compile CoqInE:

./configure make

(Type `./configure -help`

for available configuration
options.)

Start enjoying

cd t coqc test.v ../bin/coqine -h test.vo dedukti Coq1univ.dk test.dk | lua -l dedukti -

A development version of CoqInE can also been retrieved via github.

## Documentation

A succinct manual (not up-to-date) is provided with the sources
(`doc/coqine.1.gz`

). The translation itself is
explained in the following paper:

CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo, presented at the PxTP'12 workshop. .pdf

.