diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-05 20:18:58 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-01-11 09:49:32 +0100 |
| commit | 063fbe9077e6b75f327dd105774c3b3b77bda5c9 (patch) | |
| tree | 8d0cf02c3bffe27073084f55b899db05461e1299 /plugins/extraction/extraction.ml | |
| parent | d15d8cc0ce584a6d80d878faf84314c6712ccf69 (diff) | |
Extraction : some more support functions for a future "Extraction Compute"
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0be0a882b..a0e61c3b3 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1055,6 +1055,15 @@ let extract_with_type env c = Some (vl, t) | _ -> None +let extract_constr env c = + reset_meta_count (); + let typ = type_of env c in + match flag_of_type env typ with + | (_,TypeScheme) -> MLdummy, Tdummy Ktype + | (Logic,_) -> MLdummy, Tdummy Kother + | (Info,Default) -> + let mlt = extract_type env [] 1 typ [] in + extract_term env Mlenv.empty mlt c [], mlt let extract_inductive env kn = let ind = extract_ind env kn in |