diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-12 09:37:43 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-12 09:37:43 +0000 |
| commit | 9d478de763bbc2088cd7250309b2a811a5bf8c57 (patch) | |
| tree | 862fb8d645713160bc0214d4f764107401df2edf /contrib/extraction/extraction.mli | |
| parent | 9fd56d7a7281edece40240d52d25b9144d12439e (diff) | |
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2181 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/extraction.mli')
| -rw-r--r-- | contrib/extraction/extraction.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index afc6efd6f..3f71c1d89 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -26,18 +26,16 @@ type type_var = info * arity type signature = type_var list -type extraction_context = bool list - type extraction_result = | Emltype of ml_type * signature * identifier list | Emlterm of ml_ast -(*s Extraction functions. *) +(*s Extraction function. *) -val extract_constr : env -> extraction_context -> constr -> extraction_result +val extract_constr : env -> constr -> extraction_result (*s ML declaration corresponding to a Coq reference. *) val extract_declaration : global_reference -> ml_decl - +val signature : env -> constr -> signature |