diff options
author | 2014-02-24 20:46:32 +0100 | |
---|---|---|
committer | 2014-02-26 14:53:08 +0100 | |
commit | 15b6c9b6fa268a9af6dd4f05961e469545e92a6f (patch) | |
tree | 2e5aacf72993b448d1e80b0cbfbf0a09091ecb32 /plugins/extraction | |
parent | e6556db92d4c4fe9ba38f26b89f805095d2b2638 (diff) |
Lazyconstr -> Opaqueproof
Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/extract_env.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 16 |
2 files changed, 9 insertions, 9 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 5f17e0997..791294902 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -137,7 +137,7 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with | Def lbody -> - (match kind_of_term (Lazyconstr.force lbody) with + (match kind_of_term (Mod_subst.force_constr lbody) with | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> raise Impossible) 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) -> |