diff options
Diffstat (limited to 'contrib/extraction/extraction.ml')
| -rw-r--r-- | contrib/extraction/extraction.ml | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 27687ae1c..b7be86bff 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -876,6 +876,20 @@ let extract_constant_spec env kn cb = let t = snd (record_constant_type env kn (Some typ)) in Sval (r, type_expunge env t) +let extract_with_type env cb = + let typ = Typeops.type_of_constant_type env cb.const_type in + match flag_of_type env typ with + | (_ , Default) -> None + | (Logic, TypeScheme) ->Some ([],Tdummy Ktype) + | (Info, TypeScheme) -> + let s,vl = type_sign_vl env typ in + (match cb.const_body with + | None -> assert false + | Some body -> + let db = db_from_sign s in + let t = extract_type_scheme env db (force body) (List.length s) + in Some ( vl, t) ) + let extract_inductive env kn = let ind = extract_ind env kn in add_recursors env kn; @@ -903,9 +917,3 @@ let logical_spec = function | Sval (_,Tdummy _) -> true | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false - - - - - - |