From 875e410294503b03f0954c94164bd611a5682850 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Jan 2021 16:20:04 +0100
Subject: Move the two only calls to the strong combinator to their calling
 site.

---
 pretyping/tacred.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping/tacred.ml')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 01819a650b..bd21ecef93 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1040,7 +1040,10 @@ let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, [])
 let whd_simpl env sigma c =
   applist (whd_simpl_stack env sigma (c, []))
 
-let simpl env sigma c = strong whd_simpl env sigma c
+let simpl env sigma c =
+  let rec strongrec env t =
+    map_constr_with_full_binders env sigma push_rel strongrec env (whd_simpl env sigma t) in
+  strongrec env c
 
 (* Reduction at specific subterms *)
 
-- 
cgit v1.2.3