diff options
| author | Pierre-Marie Pédrot | 2020-02-11 22:07:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-04 12:44:45 +0200 |
| commit | 7a8c4003ef5071d6b9bc248e997d0397304e8491 (patch) | |
| tree | a2994e5cd0a245aa756125ceb8626bbc093f45a8 /tactics/redexpr.ml | |
| parent | e766d31683550d1debea70a3620fc3597a154700 (diff) | |
Move the cbn reduction to its own file, and simplify the RAKAM accordingly.
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 |