diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 74ea904c4..e04cad5c4 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1496,7 +1496,7 @@ let vernac_check_may_eval redexp glopt rc = | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in - let redfun = fst (reduction_of_red_expr env r_interp) in + let redfun env evm c = snd (fst (reduction_of_red_expr env r_interp) env evm c) in msg_notice (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = |