aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/extraction.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-03-20 12:57:47 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-03-20 12:57:47 +0000
commit4a232998994ee0b46f28d0b7148882ddbb5a9a00 (patch)
tree26adad3578c06efc1ae82a77d3169a89faa0ec62 /contrib/extraction/extraction.mli
parent187dc15532f0c6f380d7bcb07adc2180c29fedc2 (diff)
Extract_term_with_type. mise a jour & verification des commentaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1470 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/extraction.mli')
-rw-r--r--contrib/extraction/extraction.mli5
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index df5a414a1..b54a7b9ab 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -19,6 +19,8 @@ type type_var = Varity | Vprop | Vdefault
type signature = (type_var * identifier) list
+type extraction_context = type_var list
+
type extraction_result =
| Emltype of ml_type * signature * identifier list
| Emlterm of ml_ast
@@ -26,7 +28,8 @@ type extraction_result =
(*s Extraction functions. *)
-val extract_constr : env -> constr -> extraction_result
+val extract_constr :
+ env -> extraction_context -> constr -> extraction_result
(*s ML declaration corresponding to a Coq reference. *)