diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-07 14:01:59 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-07 14:01:59 +0000 |
| commit | 2be0079f2ed4b67eae474341a10b9f60dcf83c4f (patch) | |
| tree | 97e03cde10cff22588e9019477d16febb93fc75e /plugins/extraction/table.mli | |
| parent | 670a61a7ca4c55a5e06a79a73989a52bf0cb2273 (diff) | |
Extraction Library Foo creates Foo.ml, not foo.ml
And similarly for Haskell: we do not force capitalized/uncapitalized
filenames anymore, but we rather follow the name of the .v file (with
new extensions of course). Ok, this is an incompatible change, but
it is really convenient, some people where actually already doing
some hacks to have this behavior (cf. Compcert).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13260 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index f3da84933..18904a8b4 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -46,6 +46,7 @@ val current_toplevel : unit -> module_path val base_mp : module_path -> module_path val is_modfile : module_path -> bool val string_of_modfile : module_path -> string +val file_of_modfile : module_path -> string val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool val visible_kn : kernel_name -> bool |