diff options
Diffstat (limited to 'tactics/redexpr.ml')
| -rw-r--r-- | tactics/redexpr.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index f681e4e99e..e000ddce74 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -44,11 +44,7 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) -let whd_cbn flags env sigma t = - let (state,_) = - (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty)) - in - Reductionops.Stack.zip ~refold:true sigma state +let whd_cbn = Cbn.whd_cbn let strong_cbn flags = strong_with_flags whd_cbn flags |