diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 14 |
3 files changed, 17 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index c48882c1a..45ef3efad 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -347,10 +347,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = check_typability env sigma ty; check_conv_leq_goal env sigma trm ty conclty; let res = mk_refgoals sigma goal goalacc ty t in - (** we keep the casts (in particular VMcast) except + (** we keep the casts (in particular VMcast and NATIVEcast) except when they are annotating metas *) if isMeta t then begin - assert (k != VMcast); + assert (k != VMcast && k != NATIVEcast); res end else let (gls,cty,sigma,trm) = res in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c5a190228..ed985f292 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -270,7 +270,8 @@ let close_proof () = (fun (c,t) -> { Entries.const_entry_body = c; const_entry_secctx = section_vars; const_entry_type = Some t; - const_entry_opaque = true }) + const_entry_opaque = true; + const_entry_inline_code = false }) proofs_and_types in let { compute_guard=cg ; strength=str ; hook=hook } = diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index c4c821a9e..91ef038ee 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -28,6 +28,9 @@ let cbv_vm env _ c = let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in Vnorm.cbv_vm env c ctyp +let cbv_native env _ c = + let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in + Nativenorm.native_norm env c ctyp let set_strategy_one ref l = let k = @@ -206,7 +209,16 @@ let rec reduction_of_red_expr = function let redfun = contextually b lp vmfun in (redfun, VMcast) | CbvVm None -> (cbv_vm, VMcast) - + | CbvNative (Some lp) -> + let b = is_reference (snd lp) in + let lp = out_with_occurrences lp in + let nativefun _ env map c = + let tpe = Retyping.get_type_of env map c in + Nativenorm.native_norm env c tpe + in + let redfun = contextually b lp nativefun in + (redfun, NATIVEcast) + | CbvNative None -> (cbv_native, NATIVEcast) let subst_flags subs flags = { flags with rConst = List.map subs flags.rConst } |