From 9065877add52fa94de699ee8a50d240fb7ef4a5c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 3 Jul 2020 15:32:53 +0200
Subject: Further cleanup of dead code in the Reductionops API.

---
 pretyping/reductionops.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 20240a175d..87605c7b15 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -436,15 +436,11 @@ type state = constr * constr Stack.t
 type reduction_function = env -> evar_map -> constr -> constr
 type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 
-type contextual_stack_reduction_function =
+type stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
-type stack_reduction_function = contextual_stack_reduction_function
-type local_stack_reduction_function =
-    evar_map -> constr -> constr * constr list
 
 type state_reduction_function =
     env -> evar_map -> state -> state
-type local_state_reduction_function = evar_map -> state -> state
 
 let pr_state env sigma (tm,sk) =
   let open Pp in
-- 
cgit v1.2.3