From 73b3be7a2a4a0fd10d08aa0ca1e16050dc609943 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 20 Jan 2021 18:37:45 +0100
Subject: Factorize the call of nf_beta in red_elim_const.

---
 pretyping/tacred.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a103699716..bc7d50ccfa 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -470,7 +470,8 @@ let contract_fix_use_function env sigma f
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
   let lbodies = List.init nbodies make_Fi in
-  substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum))
+  let c = substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) in
+  nf_beta env sigma c
 
 let contract_cofix_use_function env sigma f
   (bodynum,(_names,_,bodies as typedbodies)) =
@@ -686,7 +687,7 @@ let rec red_elim_const env sigma ref u largs =
         let f = ([|Some (minfxargs,ref)|],infos), u, largs in
         (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with
            | NotReducible -> raise Redelimination
-           | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
+           | Reduced (c,rest) -> (c, rest), nocase)
     | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
         let rec descend (ref,u) args =
           let c = reference_value env sigma ref u in
@@ -700,7 +701,7 @@ let rec red_elim_const env sigma ref u largs =
         let f = refinfos, u, midargs in
         (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with
            | NotReducible -> raise Redelimination
-           | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
+           | Reduced (c,rest) -> (c, rest), nocase)
     | NotAnElimination when unfold_nonelim ->
          let c = reference_value env sigma ref u in
            (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase
-- 
cgit v1.2.3