diff options
Diffstat (limited to 'contrib/extraction/ocaml.mli')
| -rw-r--r-- | contrib/extraction/ocaml.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 5304199b7d..bda89d9372 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -39,7 +39,7 @@ val get_db_name : int -> env -> identifier val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds +val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds (*s Production of Ocaml syntax. We export both a functor to be used for extraction in the Coq toplevel and a function to extract some |