diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 0430a239e2..10e1e66cb2 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -191,7 +191,16 @@ let rec reduction_of_red_expr = function (try reduction_of_red_expr (Stringmap.find s !red_expr_tab) with Not_found -> error("unknown user-defined reduction \""^s^"\""))) - | CbvVm -> (cbv_vm ,VMcast) + | CbvVm (Some lp) -> + let b = is_reference (snd lp) in + let lp = out_with_occurrences lp in + let vmfun _ env map c = + let tpe = Retyping.get_type_of env map c in + Vnorm.cbv_vm env c tpe + in + let redfun = contextually b lp vmfun in + (redfun, VMcast) + | CbvVm None -> (cbv_vm, VMcast) let subst_flags subs flags = |