diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-23 14:22:25 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-23 14:22:25 +0000 |
| commit | a575d0cbb9321d849af020c1e7ee56f6a50daef4 (patch) | |
| tree | 78583d4ef2e6a07eed490c377ef985a7b1e6654b /contrib/extraction/ocaml.mli | |
| parent | c5de1d84957842c263fddaf7482087e7e0edfeb4 (diff) | |
eta-expansion des constructeurs si necessaire (a posteriori en miniML)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1481 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/ocaml.mli')
| -rw-r--r-- | contrib/extraction/ocaml.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index ff8dce97f..6a2834bb7 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -8,9 +8,13 @@ (*i $Id$ i*) -(*s Production of Ocaml syntax. *) +(*s Production of Ocaml syntax. We export both a functor to be used for + extraction in the Coq toplevel and a module [Pp] to be used for + production of Ocaml files. *) open Miniml module Make : functor(P : Mlpp_param) -> Mlpp +module Pp : Mlpp + |