@@ -15,5 +15,5 @@ Our formal representation of the Coq logic is untyped, i.e., we use a single typ

As we explain in Sect.~\ref{sec:logic}, we consider a typed representation infeasible at this point.

Moreover, our representation does not include the typing rules.

This is not due to a principal limitation: it is possible to add these rulesto let \mmt type-check the library.

But formalizing the Coq type system is in itself a major challenge, and representing the details of, e.g., Coq's treatment of pattern matching or sort polymorphism may even require innovations in logical framework design.

But formalizing the Coq type system is in itself a major challenge, and representing the details of, e.g., Coq's treatment of pattern matching or sort polymorphism may even require innovations in logical framework design.\ednote{DM: Talk about applications}

@@ -37,7 +37,7 @@ This overall line of research was presented in \cite{KR:qed:14}.

Similarly, to the \mmt research, proof assistant libraries have been exported into Dedukti \cite{dedukti}.

While \mmt exports focus on preserving the original structure, Dedukti exports focus on reverifying proofs.

Coqine is the tool used for translating Coq to Dedukti.

Coqine is the tool used for translating Coq to Dedukti.\ednote{@FR: rewrite this}

Unlike our logic definition, Coqine includes a formalization of the typing rules in order to type check the export.

However, this translation eliminates some features of the Coq logic in order to simplify the typing rules and, contrary to our export, does not handle the full Coq library.

The original version \cite{coqine} covered most of the small standard library.