diff options
| author | Pierre-Marie Pédrot | 2021-01-20 18:37:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-20 22:22:28 +0100 |
| commit | 73b3be7a2a4a0fd10d08aa0ca1e16050dc609943 (patch) | |
| tree | 55db4145797f68a6bb98123ea6a3c8e39942a918 | |
| parent | 07fed7d769bb6e78384c9f5312bd8a73bbb582ed (diff) | |
Factorize the call of nf_beta in red_elim_const.
| -rw-r--r-- | pretyping/tacred.ml | 7 |
1 files 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 |