diff options
| author | Pierre-Marie Pédrot | 2016-06-20 19:54:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-24 15:16:03 +0200 |
| commit | 1eea5f0081264ccb01a12f682734e8a624f83804 (patch) | |
| tree | 251df7b629e42e1c9cd2be6808b98572646f028c | |
| parent | 922ad0c1cb4a4badf4c9c2cd098285a008495519 (diff) | |
Optimization in the subst tactic.
We use simple variable substitution instead of full-power term
matching.
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c336bb434a..3ba058e7f4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2932,8 +2932,7 @@ let unfold_body x = in Tacticals.New.afterHyp x begin fun aft -> let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in - let xvar = mkVar x in - let rfun _ _ c = replace_term xvar xval c in + let rfun _ _ c = replace_vars [x, xval] c in let reducth h = reduct_in_hyp rfun h in let reductc = reduct_in_concl (rfun, DEFAULTcast) in Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc] |