aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/haskell.mli
diff options
context:
space:
mode:
authorletouzey2001-09-18 17:19:09 +0000
committerletouzey2001-09-18 17:19:09 +0000
commitf494f444ca06a573713aede990ba93a58ea4cf13 (patch)
treed6d66b1c526fcba989462ab3da0a6b1babb24a8d /contrib/extraction/haskell.mli
parent0e3358ba241414b2ec2c3448498a9fa69b2245e1 (diff)
travail sur le Extract Constant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1986 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/haskell.mli')
-rw-r--r--contrib/extraction/haskell.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 8e09da5c4c..77bea2b8b5 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -12,5 +12,7 @@
open Miniml
open Mlutil
+open Term
-val extract_to_file : string -> extraction_params -> ml_decl list -> unit
+val extract_to_file :
+ string -> extraction_params -> ml_decl list -> global_reference list -> unit