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/scheme.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/scheme.mli')
| -rw-r--r-- | contrib/extraction/scheme.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli index 84940bbe7..4bd2a3d8b 100644 --- a/contrib/extraction/scheme.mli +++ b/contrib/extraction/scheme.mli @@ -16,7 +16,8 @@ open Names 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 module Make : functor(P : Mlpp_param) -> Mlpp |