From 12d53dc64fa565ae6408d2ebb668e997b7e574b3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 10 Dec 2020 18:12:23 +0100
Subject: Extrude the computation of redexp flags in reduce.

This was a source of slowdown observed in bedrock2.
---
 tactics/tactics.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5aa31092e9..2a855e47af 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -959,17 +959,18 @@ let reduce redexp cl =
   | Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv
   | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*)
   in
+  let redexp = Redexpr.eval_red_expr env redexp in
   begin match cl.concl_occs with
   | NoOccurrences -> Proofview.tclUNIT ()
   | occs ->
     let redexp = bind_red_expr_occurrences occs nbcl redexp in
-    let redfun = Redexpr.reduction_of_red_expr env redexp in
+    let redfun = Redexpr.reduction_of_red_expr_val redexp in
     e_change_in_concl ~check (revert_cast redfun)
   end
   <*>
   let f (id, occs, where) =
     let redexp = bind_red_expr_occurrences occs nbcl redexp in
-    let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
+    let (redfun, _) = Redexpr.reduction_of_red_expr_val redexp in
     let redfun _ env sigma c = redfun env sigma c in
     let redfun env sigma d = e_pf_change_decl redfun where env sigma d in
     (id, redfun)
-- 
cgit v1.2.3