diff options
| author | coqbot-app[bot] | 2020-12-14 16:35:06 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-14 16:35:06 +0000 |
| commit | 6c35e25cfa8fd47a7aa856de005e7778b5ca0e21 (patch) | |
| tree | 4e52224047e42ae568e2030094ca470756bd6066 /pretyping/reductionops.ml | |
| parent | 8fc64949349a003d28e8a7341e3038a1ed993128 (diff) | |
| parent | d3d4bb64abf195c399cb3925292693bca29a16a4 (diff) | |
Merge PR #13630: Cleanup reductionops
Reviewed-by: gares
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3352bfce38..7a5d0897b5 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -930,14 +930,6 @@ let stack_red_of_state_red f = let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in f -(* Drops the Cst_stack *) -let iterate_whd_gen flags env sigma s = - let rec aux t = - let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in - let whd_sk = Stack.map aux sk in - Stack.zip sigma (hd,whd_sk) - in aux s - let red_of_state_red f env sigma x = Stack.zip sigma (f env sigma (x,Stack.empty)) |