diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 01:22:34 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 01:22:34 +0000 |
| commit | 7da1f2925cd7c355d38f5cfac7d5d3195f6191e9 (patch) | |
| tree | 1b16a7d57c23678e45bd4b400726c836e0c597d8 /contrib/extraction/ocaml.mli | |
| parent | 7c4ffd70946030c74105323f8b45d6d9edfa7ac0 (diff) | |
Extraction des modules, enfin !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3569 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/ocaml.mli')
| -rw-r--r-- | contrib/extraction/ocaml.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index da2706f68..babe170c2 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -27,6 +27,8 @@ val rename_id : identifier -> Idset.t -> identifier val lowercase_id : identifier -> identifier val uppercase_id : identifier -> identifier +val pr_upper_id : identifier -> std_ppcmds + type env = identifier list * Idset.t val rename_vars: Idset.t -> identifier list -> env @@ -36,7 +38,11 @@ val get_db_name : int -> env -> identifier val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds +val preamble : + extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds + +val preamble_sig : + extraction_params -> module_path list -> 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 |