diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index fb426efed..c9d4e388d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -736,10 +736,6 @@ let fix_recarg ((recindices,bodynum),_) stack = with Not_found -> None -type 'a reduced_state = - | NotReducible - | Reduced of constr - (** Generic reduction function with environment Here is where unfolded constant are stored in order to be @@ -1082,13 +1078,6 @@ let whd_betadeltaiota_stack env = let whd_betadeltaiota env = red_of_state_red (whd_betadeltaiota_state env) -let whd_betadeltaiota_state_using ts env = - raw_whd_state_gen (Closure.RedFlags.red_add_transparent betadeltaiota ts) env -let whd_betadeltaiota_stack_using ts env = - stack_red_of_state_red (whd_betadeltaiota_state_using ts env) -let whd_betadeltaiota_using ts env = - red_of_state_red (whd_betadeltaiota_state_using ts env) - let whd_betadeltaiotaeta_state env = raw_whd_state_gen betadeltaiotaeta env let whd_betadeltaiotaeta_stack env = stack_red_of_state_red (whd_betadeltaiotaeta_state env) |