From cf60564b9e6cdfa35fe8c256f6785e23a2afde61 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 Apr 2020 17:39:49 +0200
Subject: Further cleanup: remove the local_reduction_function type.

---
 pretyping/reductionops.ml  | 11 -----------
 pretyping/reductionops.mli |  3 ---
 pretyping/unification.ml   |  3 ++-
 3 files changed, 2 insertions(+), 15 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4d083664f7..15bf9667b3 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -604,7 +604,6 @@ end
 type state = constr * constr Stack.t
 
 type reduction_function = env -> evar_map -> constr -> constr
-type local_reduction_function = evar_map -> constr -> constr
 type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 
 type contextual_stack_reduction_function =
@@ -649,16 +648,6 @@ let strong whdfun env sigma t =
     map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
   strongrec env t
 
-let local_strong whdfun sigma =
-  let rec strongrec t = EConstr.map sigma strongrec (whdfun sigma t) in
-  strongrec
-
-let rec strong_prodspine redfun sigma c =
-  let x = redfun sigma c in
-  match EConstr.kind sigma x with
-    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
-    | _ -> x
-
 (*************************************)
 (*** Reduction using bindingss ***)
 (*************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 555c4be971..be91f688e7 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -128,7 +128,6 @@ end
 type state = constr * constr Stack.t
 
 type reduction_function = env -> evar_map -> constr -> constr
-type local_reduction_function = evar_map -> constr -> constr
 
 type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 
@@ -150,8 +149,6 @@ val strong_with_flags :
   (CClosure.RedFlags.reds -> reduction_function) ->
   (CClosure.RedFlags.reds -> reduction_function)
 val strong : reduction_function -> reduction_function
-val local_strong : local_reduction_function -> local_reduction_function
-val strong_prodspine : local_reduction_function -> local_reduction_function
 (*i
 val stack_reduction_of_reduction :
   'a reduction_function -> 'a state_reduction_function
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ab99bdc777..88eec5ea01 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1641,7 +1641,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   (fun test -> match test.testing_state with
   | None -> None
   | Some (sigma,_,l) ->
-     let c = applist (local_strong whd_meta sigma c, l) in
+    let rec strong_whd_meta t = EConstr.map sigma strong_whd_meta (whd_meta sigma t) in
+    let c = applist (strong_whd_meta c, l) in
      Some (sigma, c))
 
 let make_eq_test env evd c =
-- 
cgit v1.2.3