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/extraction.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/extraction.mli')
| -rw-r--r-- | contrib/extraction/extraction.mli | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index 268a68692..c9654d25c 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -10,10 +10,28 @@ (*s Extraction from Coq terms to Miniml. *) +open Names +open Term +open Declarations +open Environ open Libnames open Miniml +val extract_constant : env -> kernel_name -> constant_body -> ml_decl + +val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec + +val extract_fixpoint : + env -> kernel_name array -> (constr, types) prec_declaration -> ml_decl + +val extract_inductive : env -> kernel_name -> ml_ind + (*s ML declaration corresponding to a Coq reference. *) -val extract_declaration : global_reference -> ml_decl +val extract_declaration : env -> global_reference -> ml_decl + +(*s Without doing complete extraction, just guess what a constant would be. *) + +type kind = Logical | Term | Type +val constant_kind : env -> constant_body -> kind |