diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6fc1973d0..134e01ee1 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -285,7 +285,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> mlt | Def _ when is_custom r -> mlt | Def lbody -> - let newc = applist (Lazyconstr.force lbody, args) in + let newc = applist (Mod_subst.force_constr lbody, args) in let mlt' = extract_type env db j newc [] in (* ML type abbreviations interact badly with Coq *) (* reduction, so [mlt] and [mlt'] might be different: *) @@ -299,7 +299,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) - let newc = applist (Lazyconstr.force lbody, args) in + let newc = applist (Mod_subst.force_constr lbody, args) in extract_type env db j newc [])) | Ind (kn,i) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in @@ -523,7 +523,7 @@ and mlt_env env r = match r with | Def l_body -> (match flag_of_type env typ with | Info,TypeScheme -> - let body = Lazyconstr.force l_body in + let body = Mod_subst.force_constr l_body in let s,vl = type_sign_vl env typ in let db = db_from_sign s in let t = extract_type_scheme env db body (List.length s) @@ -995,20 +995,20 @@ let extract_constant env kn cb = | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () - | Def c -> mk_typ (Lazyconstr.force c) + | Def c -> mk_typ (Mod_subst.force_constr c) | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_typ (Lazyconstr.force_opaque c) + mk_typ (Opaqueproof.force_proof c) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () - | Def c -> mk_def (Lazyconstr.force c) + | Def c -> mk_def (Mod_subst.force_constr c) | OpaqueDef c -> add_opaque r; if access_opaque () then - mk_def (Lazyconstr.force_opaque c) + mk_def (Opaqueproof.force_proof c) else mk_ax ()) let extract_constant_spec env kn cb = @@ -1023,7 +1023,7 @@ let extract_constant_spec env kn cb = | Undef _ | OpaqueDef _ -> Stype (r, vl, None) | Def body -> let db = db_from_sign s in - let body = Lazyconstr.force body in + let body = Mod_subst.force_constr body in let t = extract_type_scheme env db body (List.length s) in Stype (r, vl, Some t)) | (Info, Default) -> |