From 78a0d0a557f4fb6885987e99c4a12a0826d48c9a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Dec 2020 00:51:52 +0100
Subject: Remove most of Reductionops.*_state functions.

There functions export the internal stack representation. The only real user
is unification, which is suffering from major performance issues due to the
naive representation of substitutions in processes.
---
 pretyping/reductionops.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'pretyping/reductionops.ml')

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))
 
-- 
cgit v1.2.3