Rewriting the proof monad mechanism. Now it uses pure OCaml code, without

going through a Coq extraction phase.

We use second order quantification through OCaml records, which allows for
a very precise use of low-level application. This results in quite a remarkable
speedup but there is still room for improvement.

This code was written by translating straightforwardly the Coq generated code
in a human-readable dialect.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17068 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions