From 4ebabae43d526a949b510c8cead511bdef899bfe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 7 Jul 2023 20:25:34 +0200 Subject: [PATCH] Remove dead code in induction internals. It was known statically that ElimOver nodes could only be built with the recursive flag set to true. --- tactics/induction.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tactics/induction.ml b/tactics/induction.ml index 70834e2532ff..7b2bb83ead15 100644 --- a/tactics/induction.ml +++ b/tactics/induction.ml @@ -1022,7 +1022,7 @@ type scheme_signature = (Id.Set.t * branch_argument list) array type eliminator_source = | CaseOver of Id.t * (inductive * EInstance.t) - | ElimOver of bool * Id.t * (inductive * EInstance.t) + | ElimOver of Id.t * (inductive * EInstance.t) | ElimUsing of Id.t * (Evd.econstr with_bindings * EConstr.types * scheme_signature) | ElimUsingList of (Evd.econstr with_bindings * EConstr.types * scheme_signature) * Id.t list * Id.t list * EConstr.t list @@ -1031,7 +1031,7 @@ let find_induction_type env sigma isrec elim hyp0 sort = match elim with let is_elim, ind, typ = guess_elim_shape env sigma isrec sort hyp0 in (* We drop the scheme and elimc/elimt waiting to know if it is dependent, this needs no update to sigma at this point. *) - let elim = if is_elim then ElimOver (isrec, hyp0, ind) else CaseOver (hyp0, ind) in + let elim = if is_elim then ElimOver (hyp0, ind) else CaseOver (hyp0, ind) in sigma, typ, elim | Some (elimc, lbind as e) -> let sigma, elimt = Typing.type_of env sigma elimc in @@ -1114,7 +1114,7 @@ let apply_induction_in_context with_evars inhyps elim indvars names = let env = Proofview.Goal.env gl in let concl = Tacmach.pf_concl gl in let hyp0 = match elim with - | ElimUsing (hyp0, _) | ElimOver (_, hyp0, _) | CaseOver (hyp0, _) -> Some hyp0 + | ElimUsing (hyp0, _) | ElimOver (hyp0, _) | CaseOver (hyp0, _) -> Some hyp0 | ElimUsingList _ -> None in let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in @@ -1133,14 +1133,14 @@ let apply_induction_in_context with_evars inhyps elim indvars names = let indsign = compute_case_signature env mind dep id in let tac = destruct_tac with_evars id dep in sigma, false, tac, indsign - | ElimOver (isrec, id, (mind, u)) -> + | ElimOver (id, (mind, u)) -> let sigma, ind = find_ind_eliminator env sigma mind s in (* FIXME: we should store this instead of recomputing it *) let elimt = Retyping.get_type_of env sigma (mkConstU ind) in let scheme = compute_elim_sig sigma elimt in let indsign = compute_scheme_signature sigma scheme id (mkIndU (mind, u)) in let tac = induction_tac with_evars [] [id] (ElimConstant ind, elimt) in - sigma, isrec, tac, indsign + sigma, true, tac, indsign | ElimUsing (hyp0, (elim, elimt, indsign)) -> let tac = induction_tac with_evars [] [hyp0] (ElimClause elim, elimt) in sigma, (* bugged, should be computed *) true, tac, indsign