diff options
| author | Pierre-Marie Pédrot | 2020-06-20 13:11:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-24 15:38:24 +0200 |
| commit | 43b1742b2d7da56315fdc8e99c730fb456259cd5 (patch) | |
| tree | dadc005055714838a2b5adae87bcc5dca2a3d139 | |
| parent | 82485e9f2a36a7a52a56622a553817436636b00b (diff) | |
Remove dead code in branch_args.
| -rw-r--r-- | tactics/tacticals.ml | 7 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 |
2 files changed, 1 insertions, 8 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index a4d306c497..af10a2fae5 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -140,9 +140,7 @@ let ifOnHyp pred tac1 tac2 id gl = type branch_args = { ity : pinductive; (* the type we were eliminating on *) - largs : constr list; (* its arguments *) branchnum : int; (* the branch number *) - pred : constr; (* the predicate we used *) nassums : int; (* number of assumptions/letin to be introduced *) branchsign : bool list; (* the signature of the branch. true=assumption, false=let-in *) @@ -688,14 +686,11 @@ module New = struct in let clenv' = clenv_unique_resolver ~flags elimclause' gl in let after_tac i = - let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in let ba = { branchsign = branchsigns.(i); branchnames = brnames.(i); nassums = List.length branchsigns.(i); branchnum = i+1; - ity = ind; - largs = List.map (clenv_nf_meta clenv') largs; - pred = clenv_nf_meta clenv' hd } + ity = ind; } in tac ba in diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index eebe702259..88419af836 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -89,9 +89,7 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic type branch_args = private { ity : pinductive; (** the type we were eliminating on *) - largs : constr list; (** its arguments *) branchnum : int; (** the branch number *) - pred : constr; (** the predicate we used *) nassums : int; (** number of assumptions/letin to be introduced *) branchsign : bool list; (** the signature of the branch. true=assumption, false=let-in *) |